Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove subspace_topology X Tx X = Tx.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ subspace_topology X Tx X.
We will prove U ∈ Tx.
We prove the intermediate claim Hex: ∃V ∈ Tx, U = V ∩ X.
An exact proof term for the current goal is (subspace_topologyE X Tx X U HU).
Apply Hex to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ X) HVpair).
We prove the intermediate claim HUeq: U = V ∩ X.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ X) HVpair).
We prove the intermediate claim HVsub: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HV).
We prove the intermediate claim HVeql: V ∩ X = V.
An exact proof term for the current goal is (binintersect_Subq_eq_1 V X HVsub).
We prove the intermediate claim HUeqV: U = V.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HVeql.
rewrite the current goal using HUeqV (from left to right).
An exact proof term for the current goal is HV.
Let U be given.
Assume HU: U ∈ Tx.
We will prove U ∈ subspace_topology X Tx X.
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsub).
We prove the intermediate claim Hex: ∃V ∈ Tx, U = V ∩ X.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
We will prove U = U ∩ X.
rewrite the current goal using (binintersect_Subq_eq_1 U X HUsub) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ X) U HUpow Hex).
∎