Let X, Tx, A, B, U and V be given.
Assume HTx: topology_on X Tx.
Assume HA: A ∈ Tx.
Assume HB: B ∈ Tx.
Assume Hdisj: A ∩ B = Empty.
Assume HU: U ∈ subspace_topology X Tx A.
Assume HV: V ∈ subspace_topology X Tx B.
We will prove (U ∪ V) ∈ subspace_topology X Tx (A ∪ B).
We prove the intermediate claim HUpowA: U ∈ 𝒫 A.
An exact proof term for the current goal is (SepE1 (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ A) U HU).
We prove the intermediate claim HUsubA: U ⊆ A.
An exact proof term for the current goal is (PowerE A U HUpowA).
We prove the intermediate claim HexWU: ∃W ∈ Tx, U = W ∩ A.
An exact proof term for the current goal is (SepE2 (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ A) U HU).
Apply HexWU to the current goal.
Let WU be given.
Assume HWUpair.
We prove the intermediate claim HWUinTx: WU ∈ Tx.
An exact proof term for the current goal is (andEL (WU ∈ Tx) (U = WU ∩ A) HWUpair).
We prove the intermediate claim HUeq: U = WU ∩ A.
An exact proof term for the current goal is (andER (WU ∈ Tx) (U = WU ∩ A) HWUpair).
We prove the intermediate claim HUAinTx: WU ∩ A ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx WU A HTx HWUinTx HA).
We prove the intermediate claim HUinTx: U ∈ Tx.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HUAinTx.
We prove the intermediate claim HVpowB: V ∈ 𝒫 B.
An exact proof term for the current goal is (SepE1 (𝒫 B) (λV0 : set ⇒ ∃W ∈ Tx, V0 = W ∩ B) V HV).
We prove the intermediate claim HVsubB: V ⊆ B.
An exact proof term for the current goal is (PowerE B V HVpowB).
We prove the intermediate claim HexWV: ∃W ∈ Tx, V = W ∩ B.
An exact proof term for the current goal is (SepE2 (𝒫 B) (λV0 : set ⇒ ∃W ∈ Tx, V0 = W ∩ B) V HV).
Apply HexWV to the current goal.
Let WV be given.
Assume HWVpair.
We prove the intermediate claim HWVinTx: WV ∈ Tx.
An exact proof term for the current goal is (andEL (WV ∈ Tx) (V = WV ∩ B) HWVpair).
We prove the intermediate claim HVeql: V = WV ∩ B.
An exact proof term for the current goal is (andER (WV ∈ Tx) (V = WV ∩ B) HWVpair).
We prove the intermediate claim HVBinTx: WV ∩ B ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx WV B HTx HWVinTx HB).
We prove the intermediate claim HVinTx: V ∈ Tx.
rewrite the current goal using HVeql (from left to right).
An exact proof term for the current goal is HVBinTx.
We prove the intermediate claim HUVinTx: (U ∪ V) ∈ Tx.
An exact proof term for the current goal is (topology_binunion_closed X Tx U V HTx HUinTx HVinTx).
We prove the intermediate claim HAsubAB: A ⊆ A ∪ B.
An exact proof term for the current goal is (binunion_Subq_1 A B).
We prove the intermediate claim HBsubAB: B ⊆ A ∪ B.
An exact proof term for the current goal is (binunion_Subq_2 A B).
We prove the intermediate claim HUsubAB: U ⊆ A ∪ B.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ A ∪ B.
An exact proof term for the current goal is (HAsubAB x (HUsubA x Hx)).
We prove the intermediate claim HVsubAB: V ⊆ A ∪ B.
Let x be given.
Assume Hx: x ∈ V.
We will prove x ∈ A ∪ B.
An exact proof term for the current goal is (HBsubAB x (HVsubB x Hx)).
We prove the intermediate claim HUVsubAB: (U ∪ V) ⊆ A ∪ B.
An exact proof term for the current goal is (binunion_Subq_min U V (A ∪ B) HUsubAB HVsubAB).
We prove the intermediate claim HUVpowAB: (U ∪ V) ∈ 𝒫 (A ∪ B).
An exact proof term for the current goal is (PowerI (A ∪ B) (U ∪ V) HUVsubAB).
We prove the intermediate claim HPred: ∃W ∈ Tx, (U ∪ V) = W ∩ (A ∪ B).
We use (U ∪ V) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUVinTx.
We will prove (U ∪ V) = (U ∪ V) ∩ (A ∪ B).
We prove the intermediate claim Heq: (U ∪ V) ∩ (A ∪ B) = (U ∪ V).
An exact proof term for the current goal is (binintersect_Subq_eq_1 (U ∪ V) (A ∪ B) HUVsubAB).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 (A ∪ B)) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ (A ∪ B)) (U ∪ V) HUVpowAB HPred).
∎