Let X, Tx and Y be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
We will prove topology_on Y (subspace_topology X Tx Y).
We will prove subspace_topology X Tx Y ⊆ 𝒫 Y ∧ Empty ∈ subspace_topology X Tx Y ∧ Y ∈ subspace_topology X Tx Y ∧ (∀UFam ∈ 𝒫 (subspace_topology X Tx Y), ⋃ UFam ∈ subspace_topology X Tx Y) ∧ (∀U ∈ subspace_topology X Tx Y, ∀V ∈ subspace_topology X Tx Y, U ∩ V ∈ subspace_topology X Tx Y).
Apply andI to the current goal.
We will prove (subspace_topology X Tx Y ⊆ 𝒫 Y ∧ Empty ∈ subspace_topology X Tx Y) ∧ Y ∈ subspace_topology X Tx Y ∧ (∀UFam ∈ 𝒫 (subspace_topology X Tx Y), ⋃ UFam ∈ subspace_topology X Tx Y).
Apply andI to the current goal.
We will prove subspace_topology X Tx Y ⊆ 𝒫 Y ∧ Empty ∈ subspace_topology X Tx Y ∧ Y ∈ subspace_topology X Tx Y.
Apply andI to the current goal.
We will prove subspace_topology X Tx Y ⊆ 𝒫 Y ∧ Empty ∈ subspace_topology X Tx Y.
Apply andI to the current goal.
We will prove subspace_topology X Tx Y ⊆ 𝒫 Y.
Let U be given.
Assume HU: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topology_in_Power X Tx Y U HU).
We will prove Empty ∈ subspace_topology X Tx Y.
We prove the intermediate claim HEmptyTx: Empty ∈ Tx.
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
We prove the intermediate claim HPred: ∃V ∈ Tx, Empty = V ∩ Y.
We use Empty to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HEmptyTx.
We will prove Empty = Empty ∩ Y.
We prove the intermediate claim H1: Empty ∩ Y = Empty.
Apply Empty_Subq_eq to the current goal.
An exact proof term for the current goal is (binintersect_Subq_1 Empty Y).
rewrite the current goal using H1 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ Y) Empty (Empty_In_Power Y) HPred).
We will prove Y ∈ subspace_topology X Tx Y.
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HPredY: ∃V ∈ Tx, Y = V ∩ Y.
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HXTx.
We will prove Y = X ∩ Y.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
Apply binintersectI to the current goal.
An exact proof term for the current goal is (HY y Hy).
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (binintersect_Subq_2 X Y).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ Y) Y (Self_In_Power Y) HPredY).
We will prove ∀UFam ∈ 𝒫 (subspace_topology X Tx Y), ⋃ UFam ∈ subspace_topology X Tx Y.
Let UFam be given.
Assume HUFam: UFam ∈ 𝒫 (subspace_topology X Tx Y).
We will prove ⋃ UFam ∈ subspace_topology X Tx Y.
We prove the intermediate claim HUFamsub: UFam ⊆ subspace_topology X Tx Y.
An exact proof term for the current goal is (PowerE (subspace_topology X Tx Y) UFam HUFam).
An exact proof term for the current goal is (subspace_topology_union_closed X Tx Y UFam HTx HY HUFamsub).
We will prove ∀U ∈ subspace_topology X Tx Y, ∀V ∈ subspace_topology X Tx Y, U ∩ V ∈ subspace_topology X Tx Y.
Let U be given.
Assume HU: U ∈ subspace_topology X Tx Y.
Let V be given.
Assume HV: V ∈ subspace_topology X Tx Y.
We will prove U ∩ V ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topology_binintersect X Tx Y U V HTx HY HU HV).
∎