Let X be given.
We will prove indiscrete_topology X ⊆ 𝒫 X ∧ Empty ∈ indiscrete_topology X ∧ X ∈ indiscrete_topology X ∧ (∀UFam ∈ 𝒫 (indiscrete_topology X), ⋃ UFam ∈ indiscrete_topology X) ∧ (∀U ∈ indiscrete_topology X, ∀V ∈ indiscrete_topology X, U ∩ V ∈ indiscrete_topology X).
Apply and5I to the current goal.
Let U be given.
Assume HU: U ∈ indiscrete_topology X.
Apply UPairE U Empty X HU to the current goal.
Assume HUe: U = Empty.
rewrite the current goal using HUe (from left to right).
An exact proof term for the current goal is (Empty_In_Power X).
Assume HUX: U = X.
rewrite the current goal using HUX (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 (UPairI1 Empty X).
An exact proof term for the current goal is (UPairI2 Empty X).
We will prove ∀UFam ∈ 𝒫 (indiscrete_topology X), ⋃ UFam ∈ indiscrete_topology X.
Let UFam be given.
Assume Hfam: UFam ∈ 𝒫 (indiscrete_topology X).
We prove the intermediate claim Hsub: UFam ⊆ indiscrete_topology X.
An exact proof term for the current goal is (PowerE (indiscrete_topology X) UFam Hfam).
Apply xm (∃U : set, U ∈ UFam ∧ U = X) to the current goal.
Assume Hex: ∃U : set, U ∈ UFam ∧ U = X.
We prove the intermediate claim HUnion_sub: ⋃ UFam ⊆ X.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUtop: U ∈ indiscrete_topology X.
An exact proof term for the current goal is (Hsub U HUin).
Apply UPairE U Empty X HUtop to the current goal.
Assume HUe: U = Empty.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using HUe (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 ∈ X)).
Assume HUX: U = X.
rewrite the current goal using HUX (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HX_sub: X ⊆ ⋃ UFam.
Let x be given.
Assume HxX.
Apply Hex to the current goal.
Let U be given.
Assume HUinpair: U ∈ UFam ∧ U = X.
We prove the intermediate claim HUin: U ∈ UFam.
An exact proof term for the current goal is (andEL (U ∈ UFam) (U = X) HUinpair).
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (andER (U ∈ UFam) (U = X) HUinpair).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxX.
Apply UnionI UFam x U HxU HUin to the current goal.
We prove the intermediate claim HUnion_eq: ⋃ UFam = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUnion_sub.
An exact proof term for the current goal is HX_sub.
rewrite the current goal using HUnion_eq (from left to right).
An exact proof term for the current goal is (UPairI2 Empty X).
Assume Hnone: ¬ ∃U : set, U ∈ UFam ∧ U = X.
We prove the intermediate claim HUnion_empty: ⋃ UFam = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUtop: U ∈ indiscrete_topology X.
An exact proof term for the current goal is (Hsub U HUin).
Apply UPairE U Empty X HUtop to the current goal.
Assume HUe: U = Empty.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HxEmpty.
Assume HUX: U = X.
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin.
An exact proof term for the current goal is HUX.
rewrite the current goal using HUnion_empty (from left to right).
An exact proof term for the current goal is (UPairI1 Empty X).
We will prove ∀U ∈ indiscrete_topology X, ∀V ∈ indiscrete_topology X, U ∩ V ∈ indiscrete_topology X.
Let U be given.
Assume HU: U ∈ indiscrete_topology X.
Let V be given.
Assume HV: V ∈ indiscrete_topology X.
Apply UPairE U Empty X HU to the current goal.
Assume HUe: U = Empty.
We prove the intermediate claim Hcap: U ∩ V = Empty.
rewrite the current goal using HUe (from left to right).
Apply Empty_Subq_eq to the current goal.
An exact proof term for the current goal is (binintersect_Subq_1 Empty V).
rewrite the current goal using Hcap (from left to right).
An exact proof term for the current goal is (UPairI1 Empty X).
Assume HUX: U = X.
Apply UPairE V Empty X HV to the current goal.
Assume HVe: V = Empty.
We prove the intermediate claim Hcap: U ∩ V = Empty.
rewrite the current goal using HVe (from left to right).
Apply Empty_Subq_eq to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 U Empty).
rewrite the current goal using Hcap (from left to right).
An exact proof term for the current goal is (UPairI1 Empty X).
Assume HVX: V = X.
We prove the intermediate claim Hcap: U ∩ V = X.
Apply set_ext to the current goal.
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
An exact proof term for the current goal is (binintersect_Subq_1 X X).
Let x be given.
Assume HxX.
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
An exact proof term for the current goal is (binintersectI X X x HxX HxX).
rewrite the current goal using Hcap (from left to right).
An exact proof term for the current goal is (UPairI2 Empty X).
∎