Let X, A and B be given.
Assume HAB HBX.
Set T0 to be the term UPair Empty A ∪ {B}.
Set T to be the term T0 ∪ {X}.
We prove the intermediate claim HA_X: A ⊆ X.
An exact proof term for the current goal is (Subq_tra A B X HAB HBX).
We prove the intermediate claim HTPow: T ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ T.
We will prove U ∈ 𝒫 X.
Apply (binunionE' T0 {X} U (U ∈ 𝒫 X)) to the current goal.
Assume HU0: U ∈ T0.
Apply (binunionE' (UPair Empty A) {B} U (U ∈ 𝒫 X)) to the current goal.
Assume HU1: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU1) 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_X).
Assume HU1: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HU1).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI X B HBX).
An exact proof term for the current goal is HU0.
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 T0 {X} Empty (binunionI1 (UPair Empty A) {B} Empty (UPairI1 Empty A))).
We prove the intermediate claim HXIn: X ∈ T.
An exact proof term for the current goal is (binunionI2 T0 {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 (B ∈ UFam)) to the current goal.
Assume HBUF: B ∈ UFam.
We prove the intermediate claim HUnionSub: ⋃ UFam ⊆ B.
Let x be given.
Assume Hx: x ∈ ⋃ UFam.
We will prove x ∈ B.
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' T0 {X} U (x ∈ B)) to the current goal.
Assume HU0: U ∈ T0.
Apply (binunionE' (UPair Empty A) {B} U (x ∈ B)) to the current goal.
Assume HU1: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU1) 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 ∈ B)).
Assume HUeq: U = A.
We prove the intermediate claim HxA: x ∈ A.
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 (HAB x HxA).
Assume HU1: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HU1).
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 HU0.
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 = B.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUnionSub.
Let x be given.
Assume HxB: x ∈ B.
An exact proof term for the current goal is (UnionI UFam x B HxB HBUF).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} B (binunionI2 (UPair Empty A) {B} B (SingI B))).
Assume HBnot: B ∉ 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' T0 {X} U (x ∈ A)) to the current goal.
Assume HU0: U ∈ T0.
Apply (binunionE' (UPair Empty A) {B} U (x ∈ A)) to the current goal.
Assume HU1: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU1) 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 HU1: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HU1).
Apply FalseE to the current goal.
We prove the intermediate claim HBUF2: B ∈ 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 (HBnot HBUF2).
An exact proof term for the current goal is HU0.
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 T0 {X} A (binunionI1 (UPair Empty A) {B} 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' T0 {X} U (x ∈ Empty)) to the current goal.
Assume HU0: U ∈ T0.
Apply (binunionE' (UPair Empty A) {B} U (x ∈ Empty)) to the current goal.
Assume HU1: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU1) 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 HU1: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HU1).
Apply FalseE to the current goal.
We prove the intermediate claim HBUF2: B ∈ 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 (HBnot HBUF2).
An exact proof term for the current goal is HU0.
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' T0 {X} U (U ∩ V ∈ T)) to the current goal.
Assume HU0: U ∈ T0.
Apply (binunionE' (UPair Empty A) {B} U (U ∩ V ∈ T)) to the current goal.
Assume HU1: U ∈ UPair Empty A.
Apply (UPairE U Empty A HU1) 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' T0 {X} V (A ∩ V ∈ T)) to the current goal.
Assume HV0: V ∈ T0.
Apply (binunionE' (UPair Empty A) {B} V (A ∩ V ∈ T)) to the current goal.
Assume HV1: V ∈ UPair Empty A.
Apply (UPairE V Empty A HV1) 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 T0 {X} A (binunionI1 (UPair Empty A) {B} A (UPairI2 Empty A))).
Assume HV1: V ∈ {B}.
We prove the intermediate claim HVeq: V = B.
An exact proof term for the current goal is (SingE B V HV1).
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: A ∩ B = A.
An exact proof term for the current goal is (binintersect_Subq_eq_1 A B HAB).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} A (binunionI1 (UPair Empty A) {B} A (UPairI2 Empty A))).
An exact proof term for the current goal is HV0.
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_X).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} A (binunionI1 (UPair Empty A) {B} A (UPairI2 Empty A))).
An exact proof term for the current goal is HV.
Assume HU1: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HU1).
rewrite the current goal using HUeq (from left to right).
Apply (binunionE' T0 {X} V (B ∩ V ∈ T)) to the current goal.
Assume HV0: V ∈ T0.
Apply (binunionE' (UPair Empty A) {B} V (B ∩ V ∈ T)) to the current goal.
Assume HV1: V ∈ UPair Empty A.
Apply (UPairE V Empty A HV1) to the current goal.
Assume HVeq: V = Empty.
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: B ∩ Empty = Empty.
An exact proof term for the current goal is (binintersect_Empty_right B).
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: B ∩ A = A.
rewrite the current goal using (binintersect_com B A) (from left to right).
An exact proof term for the current goal is (binintersect_Subq_eq_1 A B HAB).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} A (binunionI1 (UPair Empty A) {B} A (UPairI2 Empty A))).
Assume HV1: V ∈ {B}.
We prove the intermediate claim HVeq: V = B.
An exact proof term for the current goal is (SingE B V HV1).
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HcapEq: B ∩ B = B.
An exact proof term for the current goal is (binintersect_Subq_eq_1 B B (Subq_ref B)).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} B (binunionI2 (UPair Empty A) {B} B (SingI B))).
An exact proof term for the current goal is HV0.
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: B ∩ X = B.
An exact proof term for the current goal is (binintersect_Subq_eq_1 B X HBX).
rewrite the current goal using HcapEq (from left to right).
An exact proof term for the current goal is (binunionI1 T0 {X} B (binunionI2 (UPair Empty A) {B} B (SingI B))).
An exact proof term for the current goal is HV.
An exact proof term for the current goal is HU0.
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.
∎