Let X, Tx, Y and A be given.
Assume Htop: topology_on X Tx.
Assume HY: Y ⊆ X.
Assume HA: A ⊆ Y.
We will prove subspace_topology Y (subspace_topology X Tx Y) A = subspace_topology X Tx A.
Apply set_ext to the current goal.
Let W be given.
Assume HW: W ∈ subspace_topology Y (subspace_topology X Tx Y) A.
We will prove W ∈ subspace_topology X Tx A.
We prove the intermediate claim HWPowerA: W ∈ 𝒫 A.
An exact proof term for the current goal is (SepE1 (𝒫 A) (λU0 : set ⇒ ∃U ∈ subspace_topology X Tx Y, U0 = U ∩ A) W HW).
We prove the intermediate claim HWexists: ∃U ∈ subspace_topology X Tx Y, W = U ∩ A.
An exact proof term for the current goal is (subspace_topologyE Y (subspace_topology X Tx Y) A W HW).
Apply HWexists to the current goal.
Let U be given.
Assume HU: U ∈ subspace_topology X Tx Y ∧ W = U ∩ A.
We prove the intermediate claim HUinSubY: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andEL (U ∈ subspace_topology X Tx Y) (W = U ∩ A) HU).
We prove the intermediate claim HWeqUA: W = U ∩ A.
An exact proof term for the current goal is (andER (U ∈ subspace_topology X Tx Y) (W = U ∩ A) HU).
We prove the intermediate claim HUPowerY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (subspace_topology_in_Power X Tx Y U HUinSubY).
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 HUinSubY).
Apply HUexists to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ U = V ∩ Y.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HV).
We prove the intermediate claim HUeqVY: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HV).
We prove the intermediate claim HWeqVA: W = V ∩ A.
rewrite the current goal using HWeqUA (from left to right).
rewrite the current goal using HUeqVY (from left to right).
An exact proof term for the current goal is (binintersect_right_absorb_subset V Y A HA).
We prove the intermediate claim HWPred: ∃V0 ∈ Tx, W = V0 ∩ A.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVinTx.
An exact proof term for the current goal is HWeqVA.
An exact proof term for the current goal is (SepI (𝒫 A) (λW0 : set ⇒ ∃V0 ∈ Tx, W0 = V0 ∩ A) W HWPowerA HWPred).
Let W be given.
Assume HW: W ∈ subspace_topology X Tx A.
We will prove W ∈ subspace_topology Y (subspace_topology X Tx Y) A.
We prove the intermediate claim HWPowerA: W ∈ 𝒫 A.
An exact proof term for the current goal is (subspace_topology_in_Power X Tx A W HW).
We prove the intermediate claim HWexists: ∃V ∈ Tx, W = V ∩ A.
An exact proof term for the current goal is (subspace_topologyE X Tx A W HW).
Apply HWexists to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ W = V ∩ A.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (W = V ∩ A) HV).
We prove the intermediate claim HWeqVA: W = V ∩ A.
An exact proof term for the current goal is (andER (V ∈ Tx) (W = V ∩ A) HV).
Set U to be the term V ∩ Y.
We prove the intermediate claim HUinSubY: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVinTx).
We prove the intermediate claim HWeqUA: W = U ∩ A.
rewrite the current goal using HWeqVA (from left to right).
Use symmetry.
An exact proof term for the current goal is (binintersect_right_absorb_subset V Y A HA).
We prove the intermediate claim HWPred: ∃U0 ∈ subspace_topology X Tx Y, W = U0 ∩ A.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinSubY.
An exact proof term for the current goal is HWeqUA.
An exact proof term for the current goal is (SepI (𝒫 A) (λW0 : set ⇒ ∃U0 ∈ subspace_topology X Tx Y, W0 = U0 ∩ A) W HWPowerA HWPred).
∎