Let X and A be given.
Assume HA.
Set T to be the term UPair Empty A ∪ {X}.
We prove the intermediate claim HTPow: T ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ T.
We will prove U ∈ 𝒫 X.
Apply (binunionE' (UPair Empty A) {X} U (U ∈ 𝒫 X)) to the current goal.
Assume HU0: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU0) to the current goal.
Assume HUeq: U = Empty.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (Empty_In_Power X).
Assume HUeq: U = A.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI X A HA).
Assume HU0: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HU0).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (Self_In_Power X).
An exact proof term for the current goal is HU.
We prove the intermediate claim HEmptyIn: Empty ∈ T.
An exact proof term for the current goal is (binunionI1 (UPair Empty A) {X} Empty (UPairI1 Empty A)).
We prove the intermediate claim HXIn: X ∈ T.
An exact proof term for the current goal is (binunionI2 (UPair Empty A) {X} X (SingI X)).
We will prove topology_on X T.
We will prove (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) ∧ (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTPow.
An exact proof term for the current goal is HEmptyIn.
An exact proof term for the current goal is HXIn.
Let UFam be given.
Assume HUFam: UFam ∈ 𝒫 T.
We will prove ⋃ UFam ∈ T.
We prove the intermediate claim HUFsub: UFam ⊆ T.
An exact proof term for the current goal is (PowerE T UFam HUFam).
Apply (xm (X ∈ UFam)) to the current goal.
Assume HXUF: X ∈ UFam.
We prove the intermediate claim HUnionSub: ⋃ UFam ⊆ X.
We prove the intermediate claim HUFpowX: UFam ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ UFam.
An exact proof term for the current goal is (HTPow U (HUFsub U HU)).
An exact proof term for the current goal is (Union_Power X UFam HUFpowX).
We prove the intermediate claim HUnionEq: ⋃ UFam = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUnionSub.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (UnionI UFam x X HxX HXUF).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HXIn.
Assume HXnot: X ∉ UFam.
Apply (xm (A ∈ UFam)) to the current goal.
Assume HAUF: A ∈ UFam.
We prove the intermediate claim HUnionSub: ⋃ UFam ⊆ A.
Let x be given.
Assume Hx: x ∈ ⋃ UFam.
We will prove x ∈ A.
Apply UnionE_impred UFam x Hx to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUUF: U ∈ UFam.
We prove the intermediate claim HUinT: U ∈ T.
An exact proof term for the current goal is (HUFsub U HUUF).
Apply (binunionE' (UPair Empty A) {X} U (x ∈ A)) to the current goal.
Assume HU0: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU0) to the current goal.
Assume HUeq: U = Empty.
We prove the intermediate claim HxEmpty: x ∈ Empty.
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 (EmptyE x HxEmpty (x ∈ A)).
Assume HUeq: U = A.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
Assume HU0: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HU0).
Apply FalseE to the current goal.
We prove the intermediate claim HXUF2: X ∈ UFam.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUUF.
An exact proof term for the current goal is (HXnot HXUF2).
An exact proof term for the current goal is HUinT.
We prove the intermediate claim HUnionEq: ⋃ UFam = A.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUnionSub.
Let x be given.
Assume HxA: x ∈ A.
An exact proof term for the current goal is (UnionI UFam x A HxA HAUF).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair Empty A) {X} A (UPairI2 Empty A)).
Assume HAnot: A ∉ UFam.
We prove the intermediate claim HUnionEq: ⋃ UFam = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ UFam.
We will prove x ∈ Empty.
Apply UnionE_impred UFam x Hx to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUUF: U ∈ UFam.
We prove the intermediate claim HUinT: U ∈ T.
An exact proof term for the current goal is (HUFsub U HUUF).
Apply (binunionE' (UPair Empty A) {X} U (x ∈ Empty)) to the current goal.
Assume HU0: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU0) to the current goal.
Assume HUeq: U = Empty.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
Assume HUeq: U = A.
Apply FalseE to the current goal.
We prove the intermediate claim HAUF2: A ∈ UFam.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUUF.
An exact proof term for the current goal is (HAnot HAUF2).
Assume HU0: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HU0).
Apply FalseE to the current goal.
We prove the intermediate claim HXUF2: X ∈ UFam.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUUF.
An exact proof term for the current goal is (HXnot HXUF2).
An exact proof term for the current goal is HUinT.
Let x be given.
Assume Hx: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ ⋃ UFam)).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HEmptyIn.
Let U be given.
Assume HU: U ∈ T.
Let V be given.
Assume HV: V ∈ T.
We will prove U ∩ V ∈ T.
Apply (binunionE' (UPair Empty A) {X} U (U ∩ V ∈ T)) to the current goal.
Assume HU0: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU0) to the current goal.
Assume HUeq: U = Empty.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HcapEq: Empty ∩ V = Empty.
An exact proof term for the current goal is (binintersect_Empty_left V).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is HEmptyIn.
Assume HUeq: U = A.
rewrite the current goal using HUeq (from left to right).
Apply (binunionE' (UPair Empty A) {X} V (A ∩ V ∈ T)) to the current goal.
Assume HV0: V ∈ UPair Empty A.
Apply (UPairE V Empty A HV0) to the current goal.
Assume HVeq: V = Empty.
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: A ∩ Empty = Empty.
An exact proof term for the current goal is (binintersect_Empty_right A).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is HEmptyIn.
Assume HVeq: V = A.
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: A ∩ A = A.
An exact proof term for the current goal is (binintersect_Subq_eq_1 A A (Subq_ref A)).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair Empty A) {X} A (UPairI2 Empty A)).
Assume HV0: V ∈ {X}.
We prove the intermediate claim HVeq: V = X.
An exact proof term for the current goal is (SingE X V HV0).
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: A ∩ X = A.
An exact proof term for the current goal is (binintersect_Subq_eq_1 A X HA).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair Empty A) {X} A (UPairI2 Empty A)).
An exact proof term for the current goal is HV.
Assume HU0: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HU0).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
An exact proof term for the current goal is (HTPow V HV).
We prove the intermediate claim HVsub: V ⊆ X.
An exact proof term for the current goal is (PowerE X V HVpow).
We prove the intermediate claim HcapEq: X ∩ V = V.
rewrite the current goal using (binintersect_com X V) (from left to right).
An exact proof term for the current goal is (binintersect_Subq_eq_1 V X HVsub).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is HV.
An exact proof term for the current goal is HU.
∎