Let X and T be given.
Assume HT: topology_on X T.
We will prove let C ≔ {X ∖ U|U ∈ T} in X ∈ C ∧ Empty ∈ C ∧ (∀F : set, F ∈ 𝒫 C → intersection_of_family X F ∈ C) ∧ (∀A B : set, A ∈ C → B ∈ C → A ∪ B ∈ C).
Set C to be the term {X ∖ U|U ∈ T}.
We will prove X ∈ C ∧ Empty ∈ C ∧ (∀F : set, F ∈ 𝒫 C → intersection_of_family X F ∈ C) ∧ (∀A B : set, A ∈ C → B ∈ C → A ∪ B ∈ C).
We prove the intermediate claim Hempty_in_T: Empty ∈ T.
An exact proof term for the current goal is (topology_has_empty X T HT).
We prove the intermediate claim HX_in_T: X ∈ T.
An exact proof term for the current goal is (topology_has_X X T HT).
We prove the intermediate claim Hpart1: X ∈ C.
We will prove X ∈ {X ∖ U|U ∈ T}.
Apply (ReplEq T (λU ⇒ X ∖ U) X) to the current goal.
Assume _ H.
Apply H to the current goal.
We use Empty to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hempty_in_T.
We will prove X = X ∖ Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hx.
Assume Hcontra: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hcontra False).
Let x be given.
Assume Hx: x ∈ X ∖ Empty.
An exact proof term for the current goal is (setminusE1 X Empty x Hx).
We prove the intermediate claim Hpart2: X ∈ C ∧ Empty ∈ C.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart1.
We will prove Empty ∈ {X ∖ U|U ∈ T}.
Apply (ReplEq T (λU ⇒ X ∖ U) Empty) to the current goal.
Assume _ H.
Apply H to the current goal.
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HX_in_T.
We will prove Empty = X ∖ X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ X ∖ X)).
Let x be given.
Assume Hx: x ∈ X ∖ X.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X X x Hx).
We prove the intermediate claim HxnotX: x ∉ X.
An exact proof term for the current goal is (setminusE2 X X x Hx).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotX HxX).
We prove the intermediate claim Hpart3: (X ∈ C ∧ Empty ∈ C) ∧ (∀F : set, F ∈ 𝒫 C → intersection_of_family X F ∈ C).
Apply andI to the current goal.
An exact proof term for the current goal is Hpart2.
Let F be given.
Assume HF: F ∈ 𝒫 C.
We will prove intersection_of_family X F ∈ C.
Apply (xm (F = Empty)) to the current goal.
Assume HFempty: F = Empty.
We prove the intermediate claim Hintersect_empty: intersection_of_family X F = X.
rewrite the current goal using HFempty (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X Empty.
An exact proof term for the current goal is (SepE1 X (λy ⇒ ∀U0 : set, U0 ∈ Empty → y ∈ U0) x Hx).
Let x be given.
Assume Hx: x ∈ X.
We prove the intermediate claim Hvacuous: ∀U0 : set, U0 ∈ Empty → x ∈ U0.
Let U0 be given.
Assume HU: U0 ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE U0 HU).
An exact proof term for the current goal is (SepI X (λy ⇒ ∀U0 : set, U0 ∈ Empty → y ∈ U0) x Hx Hvacuous).
rewrite the current goal using Hintersect_empty (from left to right).
An exact proof term for the current goal is (andEL (X ∈ C) (Empty ∈ C) Hpart2).
Assume HFnonempty: F ≠ Empty.
Set G to be the term {U ∈ T|X ∖ U ∈ F}.
We will prove intersection_of_family X F ∈ {X ∖ U|U ∈ T}.
Apply (ReplEq T (λU ⇒ X ∖ U) (intersection_of_family X F)) to the current goal.
Assume _ H.
Apply H to the current goal.
We use (⋃ G) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HGsub: G ⊆ T.
Let U be given.
Assume HU: U ∈ G.
An exact proof term for the current goal is (SepE1 T (λU0 ⇒ X ∖ U0 ∈ F) U HU).
An exact proof term for the current goal is (topology_union_closed X T G HT HGsub).
We will prove intersection_of_family X F = X ∖ ⋃ G.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X F.
We will prove x ∈ X ∖ ⋃ G.
Apply setminusI to the current goal.
An exact proof term for the current goal is (SepE1 X (λy ⇒ ∀U0 : set, U0 ∈ F → y ∈ U0) x Hx).
Assume Hcontra: x ∈ ⋃ G.
Apply (UnionE_impred G x Hcontra) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUG: U ∈ G.
We prove the intermediate claim HXminusU_in_F: X ∖ U ∈ F.
An exact proof term for the current goal is (SepE2 T (λU0 ⇒ X ∖ U0 ∈ F) U HUG).
We prove the intermediate claim Hxall: ∀Y ∈ F, x ∈ Y.
An exact proof term for the current goal is (SepE2 X (λy ⇒ ∀U0 : set, U0 ∈ F → y ∈ U0) x Hx).
We prove the intermediate claim Hx_in_XminusU: x ∈ X ∖ U.
An exact proof term for the current goal is (Hxall (X ∖ U) HXminusU_in_F).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x Hx_in_XminusU).
An exact proof term for the current goal is (HxnotU HxU).
Let x be given.
Assume Hx: x ∈ X ∖ ⋃ G.
We will prove x ∈ intersection_of_family X F.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ G) x Hx).
We prove the intermediate claim HxnotUG: x ∉ ⋃ G.
An exact proof term for the current goal is (setminusE2 X (⋃ G) x Hx).
We will prove x ∈ {y ∈ X|∀U0 : set, U0 ∈ F → y ∈ U0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
Let Y be given.
Assume HYF: Y ∈ F.
We will prove x ∈ Y.
We prove the intermediate claim HYC: Y ∈ C.
An exact proof term for the current goal is (PowerE C F HF Y HYF).
Apply (ReplE T (λU ⇒ X ∖ U) Y HYC) to the current goal.
Let U be given.
Assume H.
Apply H to the current goal.
Assume HU: U ∈ T.
Assume HYeq: Y = X ∖ U.
We prove the intermediate claim HUG: U ∈ G.
Apply SepI to the current goal.
An exact proof term for the current goal is HU.
We will prove X ∖ U ∈ F.
rewrite the current goal using HYeq (from right to left).
An exact proof term for the current goal is HYF.
We prove the intermediate claim HxnotU: x ∉ U.
Assume Hcontra: x ∈ U.
Apply HxnotUG to the current goal.
An exact proof term for the current goal is (UnionI G x U Hcontra HUG).
rewrite the current goal using HYeq (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotU.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart3.
Let A and B be given.
Assume HA: A ∈ C.
Assume HB: B ∈ C.
We will prove A ∪ B ∈ C.
Apply (ReplE T (λU ⇒ X ∖ U) A HA) to the current goal.
Let U be given.
Assume H1.
Apply H1 to the current goal.
Assume HU: U ∈ T.
Assume HAeq: A = X ∖ U.
Apply (ReplE T (λU ⇒ X ∖ U) B HB) to the current goal.
Let V be given.
Assume H2.
Apply H2 to the current goal.
Assume HV: V ∈ T.
Assume HBeq: B = X ∖ V.
We will prove A ∪ B ∈ {X ∖ W|W ∈ T}.
Apply (ReplEq T (λW ⇒ X ∖ W) (A ∪ B)) to the current goal.
Assume _ H.
Apply H to the current goal.
We use (U ∩ V) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_binintersect_closed X T U V HT HU HV).
We will prove A ∪ B = X ∖ (U ∩ V).
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HBeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ U) ∪ (X ∖ V).
Apply (binunionE (X ∖ U) (X ∖ V) x Hx) to the current goal.
Assume HxA: x ∈ X ∖ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X U x HxA).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxA).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hcontra: x ∈ U ∩ V.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x Hcontra).
An exact proof term for the current goal is (HxnotU HxU).
Assume HxB: x ∈ X ∖ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X V x HxB).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxB).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hcontra: x ∈ U ∩ V.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x Hcontra).
An exact proof term for the current goal is (HxnotV HxV).
Let x be given.
Assume Hx: x ∈ X ∖ (U ∩ V).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (U ∩ V) x Hx).
We prove the intermediate claim HxnotUV: x ∉ U ∩ V.
An exact proof term for the current goal is (setminusE2 X (U ∩ V) x Hx).
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
We prove the intermediate claim HxnotV: x ∉ V.
Assume HxV: x ∈ V.
Apply HxnotUV to the current goal.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (setminusI X V x HxX HxnotV).
Assume HxnotU: x ∉ U.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
∎