Let X, Tx, Y and UFam be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
Assume HUFam: UFam ⊆ subspace_topology X Tx Y.
We will prove ⋃ UFam ∈ subspace_topology X Tx Y.
Set VFam to be the term {V ∈ Tx|∃U ∈ UFam, U = V ∩ Y}.
We prove the intermediate claim HVFamTx: VFam ⊆ Tx.
Let V be given.
Assume HV: V ∈ VFam.
An exact proof term for the current goal is (SepE1 Tx (λV0 ⇒ ∃U ∈ UFam, U = V0 ∩ Y) V HV).
We prove the intermediate claim HUnionVFam: ⋃ VFam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx VFam HTx HVFamTx).
We prove the intermediate claim HUnionEq: ⋃ UFam = (⋃ VFam) ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ UFam.
Apply UnionE_impred UFam x Hx to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUinFam: U ∈ UFam.
We prove the intermediate claim HUinSub: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (HUFam U HUinFam).
We prove the intermediate claim HUexists: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HUinSub).
Apply HUexists to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVpair).
Apply binintersectI to the current goal.
We will prove x ∈ ⋃ VFam.
We prove the intermediate claim HxV: x ∈ V.
We prove the intermediate claim HxVY: x ∈ V ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HVinVFam: V ∈ VFam.
Apply (SepI Tx (λV0 ⇒ ∃U0 ∈ UFam, U0 = V0 ∩ Y) V HVTx) to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinFam.
An exact proof term for the current goal is HUeq.
An exact proof term for the current goal is (UnionI VFam x V HxV HVinVFam).
We will prove x ∈ Y.
We prove the intermediate claim HxVY: x ∈ V ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
Let x be given.
Assume Hx: x ∈ (⋃ VFam) ∩ Y.
We prove the intermediate claim HxUnionV: x ∈ ⋃ VFam.
An exact proof term for the current goal is (binintersectE1 (⋃ VFam) Y x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 (⋃ VFam) Y x Hx).
Apply UnionE_impred VFam x HxUnionV to the current goal.
Let V be given.
Assume HxV: x ∈ V.
Assume HVin: V ∈ VFam.
We prove the intermediate claim HVexists: ∃U ∈ UFam, U = V ∩ Y.
An exact proof term for the current goal is (SepE2 Tx (λV0 ⇒ ∃U0 ∈ UFam, U0 = V0 ∩ Y) V HVin).
Apply HVexists to the current goal.
Let U be given.
Assume HUpair.
We prove the intermediate claim HUinFam: U ∈ UFam.
An exact proof term for the current goal is (andEL (U ∈ UFam) (U = V ∩ Y) HUpair).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (U ∈ UFam) (U = V ∩ Y) HUpair).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersectI V Y x HxV HxY).
An exact proof term for the current goal is (UnionI UFam x U HxU HUinFam).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y (⋃ VFam) HUnionVFam).
∎