Let X and Tx be given.
Assume Hreg: regular_space X Tx.
Assume Hscc: second_countable_space X Tx.
We will prove normal_space X Tx.
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).
We will prove one_point_sets_closed X Tx ∧ ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HT1.
Let A and B be given.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume HAB: A ∩ B = Empty.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx B HBcl).
We prove the intermediate claim HexBasis: ∃Basis : set, basis_on X Basis ∧ countable_set Basis ∧ basis_generates X Basis Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B0 : set, basis_on X B0 ∧ countable_set B0 ∧ basis_generates X B0 Tx) Hscc).
Apply HexBasis to the current goal.
Let Basis be given.
Assume HBasisPack: basis_on X Basis ∧ countable_set Basis ∧ basis_generates X Basis Tx.
We prove the intermediate claim HBCore: (basis_on X Basis ∧ countable_set Basis) ∧ basis_generates X Basis Tx.
An exact proof term for the current goal is HBasisPack.
We prove the intermediate claim HBasisCount: (basis_on X Basis ∧ countable_set Basis).
An exact proof term for the current goal is (andEL (basis_on X Basis ∧ countable_set Basis) (basis_generates X Basis Tx) HBCore).
We prove the intermediate claim Hgen: basis_generates X Basis Tx.
An exact proof term for the current goal is (andER (basis_on X Basis ∧ countable_set Basis) (basis_generates X Basis Tx) HBCore).
We prove the intermediate claim HBasis: basis_on X Basis.
An exact proof term for the current goal is (andEL (basis_on X Basis) (countable_set Basis) HBasisCount).
We prove the intermediate claim HBcount: countable_set Basis.
An exact proof term for the current goal is (andER (basis_on X Basis) (countable_set Basis) HBasisCount).
We prove the intermediate claim HgenEq: generated_topology X Basis = Tx.
An exact proof term for the current goal is (andER (basis_on X Basis) (generated_topology X Basis = Tx) Hgen).
We prove the intermediate claim HBasisSubTx: Basis ⊆ Tx.
Let b be given.
Assume Hb: b ∈ Basis.
We prove the intermediate claim HbGen: b ∈ generated_topology X Basis.
An exact proof term for the current goal is (generated_topology_contains_basis X Basis HBasis b Hb).
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HbGen.
Set Cand to be the term {b ∈ Basis|closure_of X Tx b ∩ B = Empty}.
We prove the intermediate claim HCandSubBasis: Cand ⊆ Basis.
Let b be given.
Assume Hb: b ∈ Cand.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) b Hb).
We prove the intermediate claim HCandCount: countable_set Cand.
An exact proof term for the current goal is (Subq_countable Cand Basis HBcount HCandSubBasis).
We prove the intermediate claim HAcover: A ⊆ ⋃ Cand.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ ⋃ Cand.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim HxnotB: x ∉ B.
Assume HxB: x ∈ B.
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HAB (from right to left).
An exact proof term for the current goal is HxAB.
An exact proof term for the current goal is (EmptyE x HxE).
Set U0 to be the term X ∖ B.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_of_closed_complement X Tx B HBcl).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (setminusI X B x HxX HxnotB).
Apply (regular_space_shrink_neighborhood X Tx x U0 Hreg HxX HU0Tx HxU0) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.
We prove the intermediate claim HV0a: (V0 ∈ Tx ∧ x ∈ V0) ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is HV0.
We prove the intermediate claim HV0b: V0 ∈ Tx ∧ x ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0a).
We prove the intermediate claim HclV0subU0: closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0a).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim HV0subX: V0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V0 HTx HV0Tx).
We prove the intermediate claim HV0openGen: open_in X (generated_topology X Basis) V0.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is (open_inI X Tx V0 HTx HV0Tx).
We prove the intermediate claim HV0eq: V0 = ⋃ {b ∈ Basis|b ⊆ V0}.
An exact proof term for the current goal is (open_as_union_of_basis_elements X Basis HBasis V0 HV0openGen).
We prove the intermediate claim HxUnion: x ∈ ⋃ {b ∈ Basis|b ⊆ V0}.
rewrite the current goal using HV0eq (from right to left).
An exact proof term for the current goal is HxV0.
Apply (UnionE_impred {b ∈ Basis|b ⊆ V0} x HxUnion) to the current goal.
Let b be given.
Assume Hxb HbFam.
We prove the intermediate claim HbBasis: b ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ b0 ⊆ V0) b HbFam).
We prove the intermediate claim HbsubV0: b ⊆ V0.
An exact proof term for the current goal is (SepE2 Basis (λb0 : set ⇒ b0 ⊆ V0) b HbFam).
We prove the intermediate claim HclbsubclV0: closure_of X Tx b ⊆ closure_of X Tx V0.
An exact proof term for the current goal is (closure_monotone X Tx b V0 HTx HbsubV0 HV0subX).
We prove the intermediate claim HclbsubU0: closure_of X Tx b ⊆ U0.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx b) (closure_of X Tx V0) U0 HclbsubclV0 HclV0subU0).
We prove the intermediate claim HclbDisjB: closure_of X Tx b ∩ B = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ (closure_of X Tx b) ∩ B.
We prove the intermediate claim Hzclb: z ∈ closure_of X Tx b.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx b) B z Hz).
We prove the intermediate claim HzB: z ∈ B.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx b) B z Hz).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (HclbsubU0 z Hzclb).
We prove the intermediate claim HznotB: z ∉ B.
An exact proof term for the current goal is (setminusE2 X B z HzU0).
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (HznotB HzB).
We prove the intermediate claim HbCand: b ∈ Cand.
An exact proof term for the current goal is (SepI Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) b HbBasis HclbDisjB).
An exact proof term for the current goal is (UnionI Cand x b Hxb HbCand).
Set Dand to be the term {b ∈ Basis|closure_of X Tx b ∩ A = Empty}.
We prove the intermediate claim HDandSubBasis: Dand ⊆ Basis.
Let b be given.
Assume Hb: b ∈ Dand.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ A = Empty) b Hb).
We prove the intermediate claim HDandCount: countable_set Dand.
An exact proof term for the current goal is (Subq_countable Dand Basis HBcount HDandSubBasis).
We prove the intermediate claim HBcover: B ⊆ ⋃ Dand.
Let x be given.
Assume HxB: x ∈ B.
We will prove x ∈ ⋃ Dand.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HBsubX x HxB).
We prove the intermediate claim HxnotA: x ∉ A.
Assume HxA: x ∈ A.
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HAB (from right to left).
An exact proof term for the current goal is HxAB.
An exact proof term for the current goal is (EmptyE x HxE).
Set U0 to be the term X ∖ A.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_of_closed_complement X Tx A HAcl).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (setminusI X A x HxX HxnotA).
Apply (regular_space_shrink_neighborhood X Tx x U0 Hreg HxX HU0Tx HxU0) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.
We prove the intermediate claim HV0a: (V0 ∈ Tx ∧ x ∈ V0) ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is HV0.
We prove the intermediate claim HV0b: V0 ∈ Tx ∧ x ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0a).
We prove the intermediate claim HclV0subU0: closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0a).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim HV0subX: V0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V0 HTx HV0Tx).
We prove the intermediate claim HV0openGen: open_in X (generated_topology X Basis) V0.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is (open_inI X Tx V0 HTx HV0Tx).
We prove the intermediate claim HV0eq: V0 = ⋃ {b ∈ Basis|b ⊆ V0}.
An exact proof term for the current goal is (open_as_union_of_basis_elements X Basis HBasis V0 HV0openGen).
We prove the intermediate claim HxUnion: x ∈ ⋃ {b ∈ Basis|b ⊆ V0}.
rewrite the current goal using HV0eq (from right to left).
An exact proof term for the current goal is HxV0.
Apply (UnionE_impred {b ∈ Basis|b ⊆ V0} x HxUnion) to the current goal.
Let b be given.
Assume Hxb HbFam.
We prove the intermediate claim HbBasis: b ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ b0 ⊆ V0) b HbFam).
We prove the intermediate claim HbsubV0: b ⊆ V0.
An exact proof term for the current goal is (SepE2 Basis (λb0 : set ⇒ b0 ⊆ V0) b HbFam).
We prove the intermediate claim HclbsubclV0: closure_of X Tx b ⊆ closure_of X Tx V0.
An exact proof term for the current goal is (closure_monotone X Tx b V0 HTx HbsubV0 HV0subX).
We prove the intermediate claim HclbsubU0: closure_of X Tx b ⊆ U0.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx b) (closure_of X Tx V0) U0 HclbsubclV0 HclV0subU0).
We prove the intermediate claim HclbDisjA: closure_of X Tx b ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ (closure_of X Tx b) ∩ A.
We prove the intermediate claim Hzclb: z ∈ closure_of X Tx b.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx b) A z Hz).
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx b) A z Hz).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (HclbsubU0 z Hzclb).
We prove the intermediate claim HznotA: z ∉ A.
An exact proof term for the current goal is (setminusE2 X A z HzU0).
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (HznotA HzA).
We prove the intermediate claim HbDand: b ∈ Dand.
An exact proof term for the current goal is (SepI Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ A = Empty) b HbBasis HclbDisjA).
An exact proof term for the current goal is (UnionI Dand x b Hxb HbDand).
Apply HCandCount to the current goal.
Let fC be given.
Assume HfC: inj Cand ω fC.
Apply HDandCount to the current goal.
Let fD be given.
Assume HfD: inj Dand ω fD.
We prove the intermediate claim HfiniteDprefix: ∀n : set, nat_p n → finite {d ∈ Dand|fD d ∈ ordsucc n}.
Let n be given.
Assume Hnat: nat_p n.
An exact proof term for the current goal is (inj_omega_preimage_ordsucc_finite Dand n fD Hnat HfD).
We prove the intermediate claim HfiniteCprefix: ∀n : set, nat_p n → finite {c ∈ Cand|fC c ∈ ordsucc n}.
Let n be given.
Assume Hnat: nat_p n.
An exact proof term for the current goal is (inj_omega_preimage_ordsucc_finite Cand n fC Hnat HfC).
Set Cand_eq to be the term λn : set ⇒ {c ∈ Cand|fC c = n}.
Set Dand_eq to be the term λn : set ⇒ {d ∈ Dand|fD d = n}.
Set Uraw to be the term λn : set ⇒ ⋃ (Cand_eq n).
Set Vraw to be the term λn : set ⇒ ⋃ (Dand_eq n).
Set Cand_pref to be the term λn : set ⇒ {c ∈ Cand|fC c ∈ ordsucc n}.
Set Dand_pref to be the term λn : set ⇒ {d ∈ Dand|fD d ∈ ordsucc n}.
Set ClDfam to be the term λn : set ⇒ {closure_of X Tx d|d ∈ Dand_pref n}.
Set ClCfam to be the term λn : set ⇒ {closure_of X Tx c|c ∈ Cand_pref n}.
Set ClD to be the term λn : set ⇒ ⋃ (ClDfam n).
Set ClC to be the term λn : set ⇒ ⋃ (ClCfam n).
Set Uprime to be the term λn : set ⇒ (Uraw n) ∩ (X ∖ (ClD n)).
Set Vprime to be the term λn : set ⇒ (Vraw n) ∩ (X ∖ (ClC n)).
Set Uall to be the term ⋃ {Uprime n|n ∈ ω}.
Set Vall to be the term ⋃ {Vprime n|n ∈ ω}.
We prove the intermediate claim HUallTx: Uall ∈ Tx.
We prove the intermediate claim HUfamPow: {Uprime n|n ∈ ω} ∈ 𝒫 Tx.
We prove the intermediate claim HUsubTx: {Uprime n|n ∈ ω} ⊆ Tx.
Let U0 be given.
Assume HU0: U0 ∈ {Uprime n|n ∈ ω}.
We will prove U0 ∈ Tx.
Apply (ReplE_impred ω (λn : set ⇒ Uprime n) U0 HU0 (U0 ∈ Tx)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HU0eq: U0 = Uprime n.
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim HUnat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HDprefFin: finite (Dand_pref n).
An exact proof term for the current goal is (HfiniteDprefix n HUnat).
We prove the intermediate claim HClDfamFin: finite (ClDfam n).
An exact proof term for the current goal is (Repl_finite (λd0 : set ⇒ closure_of X Tx d0) (Dand_pref n) HDprefFin).
We prove the intermediate claim HClDfamClosed: ∀C0 : set, C0 ∈ (ClDfam n) → closed_in X Tx C0.
Let C0 be given.
Assume HC0: C0 ∈ (ClDfam n).
Apply (ReplE_impred (Dand_pref n) (λd0 : set ⇒ closure_of X Tx d0) C0 HC0 (closed_in X Tx C0)) to the current goal.
Let d0 be given.
Assume Hd0: d0 ∈ Dand_pref n.
Assume HC0eq: C0 = closure_of X Tx d0.
rewrite the current goal using HC0eq (from left to right).
We prove the intermediate claim Hd0Dand: d0 ∈ Dand.
An exact proof term for the current goal is (SepE1 Dand (λd1 : set ⇒ fD d1 ∈ ordsucc n) d0 Hd0).
We prove the intermediate claim Hd0Basis: d0 ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ A = Empty) d0 Hd0Dand).
We prove the intermediate claim Hd0Tx: d0 ∈ Tx.
An exact proof term for the current goal is (HBasisSubTx d0 Hd0Basis).
We prove the intermediate claim Hd0subX: d0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx d0 HTx Hd0Tx).
An exact proof term for the current goal is (closure_is_closed X Tx d0 HTx Hd0subX).
We prove the intermediate claim HClDclosed: closed_in X Tx (ClD n).
An exact proof term for the current goal is (finite_union_closed_in X Tx (ClDfam n) HTx HClDfamFin HClDfamClosed).
We prove the intermediate claim HcompClD: X ∖ (ClD n) ∈ Tx.
We prove the intermediate claim Hopen: open_in X Tx (X ∖ (ClD n)).
An exact proof term for the current goal is (open_of_closed_complement X Tx (ClD n) HClDclosed).
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ (ClD n)) Hopen).
We prove the intermediate claim HUrawTx: Uraw n ∈ Tx.
We prove the intermediate claim HCeqSubCand: Cand_eq n ⊆ Cand.
Let c be given.
Assume Hc: c ∈ Cand_eq n.
An exact proof term for the current goal is (SepE1 Cand (λc0 : set ⇒ fC c0 = n) c Hc).
We prove the intermediate claim HCeqSubBasis: Cand_eq n ⊆ Basis.
An exact proof term for the current goal is (Subq_tra (Cand_eq n) Cand Basis HCeqSubCand HCandSubBasis).
We prove the intermediate claim HCeqSubTx: Cand_eq n ⊆ Tx.
An exact proof term for the current goal is (Subq_tra (Cand_eq n) Basis Tx HCeqSubBasis HBasisSubTx).
We prove the intermediate claim HCeqPow: Cand_eq n ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx (Cand_eq n) HCeqSubTx).
An exact proof term for the current goal is (lemma_union_of_topology_family_open X Tx (Cand_eq n) HTx HCeqPow).
An exact proof term for the current goal is (topology_binintersect_closed X Tx (Uraw n) (X ∖ (ClD n)) HTx HUrawTx HcompClD).
An exact proof term for the current goal is (PowerI Tx {Uprime n|n ∈ ω} HUsubTx).
An exact proof term for the current goal is (lemma_union_of_topology_family_open X Tx {Uprime n|n ∈ ω} HTx HUfamPow).
We prove the intermediate claim HVallTx: Vall ∈ Tx.
We prove the intermediate claim HVfamPow: {Vprime n|n ∈ ω} ∈ 𝒫 Tx.
We prove the intermediate claim HVsubTx: {Vprime n|n ∈ ω} ⊆ Tx.
Let V0 be given.
Assume HV0: V0 ∈ {Vprime n|n ∈ ω}.
We will prove V0 ∈ Tx.
Apply (ReplE_impred ω (λn : set ⇒ Vprime n) V0 HV0 (V0 ∈ Tx)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HV0eq: V0 = Vprime n.
rewrite the current goal using HV0eq (from left to right).
We prove the intermediate claim HUnat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HCprefFin: finite (Cand_pref n).
An exact proof term for the current goal is (HfiniteCprefix n HUnat).
We prove the intermediate claim HClCfamFin: finite (ClCfam n).
An exact proof term for the current goal is (Repl_finite (λc0 : set ⇒ closure_of X Tx c0) (Cand_pref n) HCprefFin).
We prove the intermediate claim HClCfamClosed: ∀C0 : set, C0 ∈ (ClCfam n) → closed_in X Tx C0.
Let C0 be given.
Assume HC0: C0 ∈ (ClCfam n).
Apply (ReplE_impred (Cand_pref n) (λc0 : set ⇒ closure_of X Tx c0) C0 HC0 (closed_in X Tx C0)) to the current goal.
Let c0 be given.
Assume Hc0: c0 ∈ Cand_pref n.
Assume HC0eq: C0 = closure_of X Tx c0.
rewrite the current goal using HC0eq (from left to right).
We prove the intermediate claim Hc0Cand: c0 ∈ Cand.
An exact proof term for the current goal is (SepE1 Cand (λc1 : set ⇒ fC c1 ∈ ordsucc n) c0 Hc0).
We prove the intermediate claim Hc0Basis: c0 ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) c0 Hc0Cand).
We prove the intermediate claim Hc0Tx: c0 ∈ Tx.
An exact proof term for the current goal is (HBasisSubTx c0 Hc0Basis).
We prove the intermediate claim Hc0subX: c0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx c0 HTx Hc0Tx).
An exact proof term for the current goal is (closure_is_closed X Tx c0 HTx Hc0subX).
We prove the intermediate claim HClCclosed: closed_in X Tx (ClC n).
An exact proof term for the current goal is (finite_union_closed_in X Tx (ClCfam n) HTx HClCfamFin HClCfamClosed).
We prove the intermediate claim HcompClC: X ∖ (ClC n) ∈ Tx.
We prove the intermediate claim Hopen: open_in X Tx (X ∖ (ClC n)).
An exact proof term for the current goal is (open_of_closed_complement X Tx (ClC n) HClCclosed).
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ (ClC n)) Hopen).
We prove the intermediate claim HVrawTx: Vraw n ∈ Tx.
We prove the intermediate claim HDeqSubDand: Dand_eq n ⊆ Dand.
Let d be given.
Assume Hd: d ∈ Dand_eq n.
An exact proof term for the current goal is (SepE1 Dand (λd0 : set ⇒ fD d0 = n) d Hd).
We prove the intermediate claim HDeqSubBasis: Dand_eq n ⊆ Basis.
An exact proof term for the current goal is (Subq_tra (Dand_eq n) Dand Basis HDeqSubDand HDandSubBasis).
We prove the intermediate claim HDeqSubTx: Dand_eq n ⊆ Tx.
An exact proof term for the current goal is (Subq_tra (Dand_eq n) Basis Tx HDeqSubBasis HBasisSubTx).
We prove the intermediate claim HDeqPow: Dand_eq n ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx (Dand_eq n) HDeqSubTx).
An exact proof term for the current goal is (lemma_union_of_topology_family_open X Tx (Dand_eq n) HTx HDeqPow).
An exact proof term for the current goal is (topology_binintersect_closed X Tx (Vraw n) (X ∖ (ClC n)) HTx HVrawTx HcompClC).
An exact proof term for the current goal is (PowerI Tx {Vprime n|n ∈ ω} HVsubTx).
An exact proof term for the current goal is (lemma_union_of_topology_family_open X Tx {Vprime n|n ∈ ω} HTx HVfamPow).
We use Uall to witness the existential quantifier.
We use Vall to witness the existential quantifier.
We will prove Uall ∈ Tx ∧ Vall ∈ Tx ∧ A ⊆ Uall ∧ B ⊆ Vall ∧ Uall ∩ Vall = Empty.
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 HUallTx.
An exact proof term for the current goal is HVallTx.
We will prove A ⊆ Uall.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ Uall.
We prove the intermediate claim HxUnionCand: x ∈ ⋃ Cand.
An exact proof term for the current goal is (HAcover x HxA).
Apply (UnionE_impred Cand x HxUnionCand) to the current goal.
Let c be given.
Assume Hxc: x ∈ c.
Assume HcCand: c ∈ Cand.
Set n to be the term fC c.
We prove the intermediate claim HnO: n ∈ ω.
We prove the intermediate claim HfCinto: ∀u ∈ Cand, fC u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Cand, fC u ∈ ω) (∀u v ∈ Cand, fC u = fC v → u = v) HfC).
An exact proof term for the current goal is (HfCinto c HcCand).
We prove the intermediate claim HcEq: c ∈ Cand_eq n.
We prove the intermediate claim HCeqdef: Cand_eq n = {c0 ∈ Cand|fC c0 = n}.
Use reflexivity.
rewrite the current goal using HCeqdef (from left to right).
Apply (SepI Cand (λc0 : set ⇒ fC c0 = n) c HcCand) to the current goal.
Use reflexivity.
We prove the intermediate claim HxUraw: x ∈ Uraw n.
An exact proof term for the current goal is (UnionI (Cand_eq n) x c Hxc HcEq).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim HxnotClD: x ∉ (ClD n).
Assume HxClD: x ∈ (ClD n).
Apply (UnionE_impred (ClDfam n) x HxClD) to the current goal.
Let C0 be given.
Assume HxC0: x ∈ C0.
Assume HC0: C0 ∈ (ClDfam n).
Apply (ReplE_impred (Dand_pref n) (λd0 : set ⇒ closure_of X Tx d0) C0 HC0 False) to the current goal.
Let d0 be given.
Assume Hd0: d0 ∈ (Dand_pref n).
Assume HC0eq: C0 = closure_of X Tx d0.
We prove the intermediate claim Hxd0cl: x ∈ closure_of X Tx d0.
rewrite the current goal using HC0eq (from right to left).
An exact proof term for the current goal is HxC0.
We prove the intermediate claim Hd0Dand: d0 ∈ Dand.
An exact proof term for the current goal is (SepE1 Dand (λd1 : set ⇒ fD d1 ∈ ordsucc n) d0 Hd0).
We prove the intermediate claim Hd0DisjA: closure_of X Tx d0 ∩ A = Empty.
An exact proof term for the current goal is (SepE2 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ A = Empty) d0 Hd0Dand).
We prove the intermediate claim HxInt: x ∈ (closure_of X Tx d0) ∩ A.
An exact proof term for the current goal is (binintersectI (closure_of X Tx d0) A x Hxd0cl HxA).
We prove the intermediate claim HxEmp: x ∈ Empty.
rewrite the current goal using Hd0DisjA (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (EmptyE x HxEmp).
We prove the intermediate claim HxCompClD: x ∈ X ∖ (ClD n).
An exact proof term for the current goal is (setminusI X (ClD n) x HxX HxnotClD).
We prove the intermediate claim HxUprime: x ∈ (Uprime n).
An exact proof term for the current goal is (binintersectI (Uraw n) (X ∖ (ClD n)) x HxUraw HxCompClD).
We prove the intermediate claim HUpInFam: (Uprime n) ∈ {Uprime k|k ∈ ω}.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ Uprime k) n HnO).
An exact proof term for the current goal is (UnionI {Uprime k|k ∈ ω} x (Uprime n) HxUprime HUpInFam).
We will prove B ⊆ Vall.
Let x be given.
Assume HxB: x ∈ B.
We will prove x ∈ Vall.
We prove the intermediate claim HxUnionDand: x ∈ ⋃ Dand.
An exact proof term for the current goal is (HBcover x HxB).
Apply (UnionE_impred Dand x HxUnionDand) to the current goal.
Let d be given.
Assume Hxd: x ∈ d.
Assume HdDand: d ∈ Dand.
Set n to be the term fD d.
We prove the intermediate claim HnO: n ∈ ω.
We prove the intermediate claim HfDinto: ∀u ∈ Dand, fD u ∈ ω.
An exact proof term for the current goal is (andEL (∀u ∈ Dand, fD u ∈ ω) (∀u v ∈ Dand, fD u = fD v → u = v) HfD).
An exact proof term for the current goal is (HfDinto d HdDand).
We prove the intermediate claim HdEq: d ∈ Dand_eq n.
We prove the intermediate claim HDeqdef: Dand_eq n = {d0 ∈ Dand|fD d0 = n}.
Use reflexivity.
rewrite the current goal using HDeqdef (from left to right).
Apply (SepI Dand (λd0 : set ⇒ fD d0 = n) d HdDand) to the current goal.
Use reflexivity.
We prove the intermediate claim HxVraw: x ∈ Vraw n.
An exact proof term for the current goal is (UnionI (Dand_eq n) x d Hxd HdEq).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HBsubX x HxB).
We prove the intermediate claim HxnotClC: x ∉ (ClC n).
Assume HxClC: x ∈ (ClC n).
Apply (UnionE_impred (ClCfam n) x HxClC) to the current goal.
Let C0 be given.
Assume HxC0: x ∈ C0.
Assume HC0: C0 ∈ (ClCfam n).
Apply (ReplE_impred (Cand_pref n) (λc0 : set ⇒ closure_of X Tx c0) C0 HC0 False) to the current goal.
Let c0 be given.
Assume Hc0: c0 ∈ (Cand_pref n).
Assume HC0eq: C0 = closure_of X Tx c0.
We prove the intermediate claim Hxc0cl: x ∈ closure_of X Tx c0.
rewrite the current goal using HC0eq (from right to left).
An exact proof term for the current goal is HxC0.
We prove the intermediate claim Hc0Cand: c0 ∈ Cand.
An exact proof term for the current goal is (SepE1 Cand (λc1 : set ⇒ fC c1 ∈ ordsucc n) c0 Hc0).
We prove the intermediate claim Hc0DisjB: closure_of X Tx c0 ∩ B = Empty.
An exact proof term for the current goal is (SepE2 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) c0 Hc0Cand).
We prove the intermediate claim HxInt: x ∈ (closure_of X Tx c0) ∩ B.
An exact proof term for the current goal is (binintersectI (closure_of X Tx c0) B x Hxc0cl HxB).
We prove the intermediate claim HxEmp: x ∈ Empty.
rewrite the current goal using Hc0DisjB (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is (EmptyE x HxEmp).
We prove the intermediate claim HxCompClC: x ∈ X ∖ (ClC n).
An exact proof term for the current goal is (setminusI X (ClC n) x HxX HxnotClC).
We prove the intermediate claim HxVprime: x ∈ (Vprime n).
An exact proof term for the current goal is (binintersectI (Vraw n) (X ∖ (ClC n)) x HxVraw HxCompClC).
We prove the intermediate claim HVpInFam: (Vprime n) ∈ {Vprime k|k ∈ ω}.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ Vprime k) n HnO).
An exact proof term for the current goal is (UnionI {Vprime k|k ∈ ω} x (Vprime n) HxVprime HVpInFam).
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUV: x ∈ Uall ∩ Vall.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxUall: x ∈ Uall.
An exact proof term for the current goal is (binintersectE1 Uall Vall x HxUV).
We prove the intermediate claim HxVall: x ∈ Vall.
An exact proof term for the current goal is (binintersectE2 Uall Vall x HxUV).
Apply (UnionE_impred {Uprime k|k ∈ ω} x HxUall) to the current goal.
Let U0 be given.
Assume HxU0: x ∈ U0.
Assume HU0: U0 ∈ {Uprime k|k ∈ ω}.
Apply (ReplE_impred ω (λk : set ⇒ Uprime k) U0 HU0 False) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HU0eq: U0 = Uprime i.
We prove the intermediate claim HxUi: x ∈ Uprime i.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HxU0.
We prove the intermediate claim HxUraw: x ∈ Uraw i.
An exact proof term for the current goal is (binintersectE1 (Uraw i) (X ∖ (ClD i)) x HxUi).
We prove the intermediate claim HxXminusClD: x ∈ X ∖ (ClD i).
An exact proof term for the current goal is (binintersectE2 (Uraw i) (X ∖ (ClD i)) x HxUi).
We prove the intermediate claim HxnotClD: x ∉ (ClD i).
An exact proof term for the current goal is (setminusE2 X (ClD i) x HxXminusClD).
Apply (UnionE_impred {Vprime k|k ∈ ω} x HxVall) to the current goal.
Let V0 be given.
Assume HxV0: x ∈ V0.
Assume HV0: V0 ∈ {Vprime k|k ∈ ω}.
Apply (ReplE_impred ω (λk : set ⇒ Vprime k) V0 HV0 False) to the current goal.
Let j be given.
Assume HjO: j ∈ ω.
Assume HV0eq: V0 = Vprime j.
We prove the intermediate claim HxVj: x ∈ Vprime j.
rewrite the current goal using HV0eq (from right to left).
An exact proof term for the current goal is HxV0.
We prove the intermediate claim HxVraw: x ∈ Vraw j.
An exact proof term for the current goal is (binintersectE1 (Vraw j) (X ∖ (ClC j)) x HxVj).
We prove the intermediate claim HxXminusClC: x ∈ X ∖ (ClC j).
An exact proof term for the current goal is (binintersectE2 (Vraw j) (X ∖ (ClC j)) x HxVj).
We prove the intermediate claim HxnotClC: x ∉ (ClC j).
An exact proof term for the current goal is (setminusE2 X (ClC j) x HxXminusClC).
Apply (UnionE_impred (Cand_eq i) x HxUraw) to the current goal.
Let c be given.
Assume Hxc: x ∈ c.
Assume HcEq: c ∈ Cand_eq i.
We prove the intermediate claim HcCand: c ∈ Cand.
An exact proof term for the current goal is (SepE1 Cand (λc0 : set ⇒ fC c0 = i) c HcEq).
We prove the intermediate claim HfCc: fC c = i.
An exact proof term for the current goal is (SepE2 Cand (λc0 : set ⇒ fC c0 = i) c HcEq).
Apply (UnionE_impred (Dand_eq j) x HxVraw) to the current goal.
Let d be given.
Assume Hxd: x ∈ d.
Assume HdEq: d ∈ Dand_eq j.
We prove the intermediate claim HdDand: d ∈ Dand.
An exact proof term for the current goal is (SepE1 Dand (λd0 : set ⇒ fD d0 = j) d HdEq).
We prove the intermediate claim HfDd: fD d = j.
An exact proof term for the current goal is (SepE2 Dand (λd0 : set ⇒ fD d0 = j) d HdEq).
We prove the intermediate claim HiNat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i HiO).
We prove the intermediate claim HjNat: nat_p j.
An exact proof term for the current goal is (omega_nat_p j HjO).
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (nat_p_ordinal i HiNat).
We prove the intermediate claim HjOrd: ordinal j.
An exact proof term for the current goal is (nat_p_ordinal j HjNat).
Apply (ordinal_trichotomy_or_impred i j HiOrd HjOrd False) to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim HiSuccJ: i ∈ ordsucc j.
An exact proof term for the current goal is (ordsuccI1 j i Hij).
We prove the intermediate claim HcPref: c ∈ Cand_pref j.
We prove the intermediate claim HCprefdef: Cand_pref j = {c0 ∈ Cand|fC c0 ∈ ordsucc j}.
Use reflexivity.
rewrite the current goal using HCprefdef (from left to right).
Apply (SepI Cand (λc0 : set ⇒ fC c0 ∈ ordsucc j) c HcCand) to the current goal.
rewrite the current goal using HfCc (from left to right).
An exact proof term for the current goal is HiSuccJ.
We prove the intermediate claim HclcInFam: closure_of X Tx c ∈ ClCfam j.
An exact proof term for the current goal is (ReplI (Cand_pref j) (λc0 : set ⇒ closure_of X Tx c0) c HcPref).
We prove the intermediate claim HcBasis: c ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) c HcCand).
We prove the intermediate claim HcTx: c ∈ Tx.
An exact proof term for the current goal is (HBasisSubTx c HcBasis).
We prove the intermediate claim HcSubX: c ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx c HTx HcTx).
We prove the intermediate claim Hxclc: x ∈ closure_of X Tx c.
We prove the intermediate claim HcSubCl: c ⊆ closure_of X Tx c.
An exact proof term for the current goal is (subset_of_closure X Tx c HTx HcSubX).
An exact proof term for the current goal is (HcSubCl x Hxc).
We prove the intermediate claim HxClC: x ∈ ClC j.
An exact proof term for the current goal is (UnionI (ClCfam j) x (closure_of X Tx c) Hxclc HclcInFam).
An exact proof term for the current goal is (HxnotClC HxClC).
Assume HijEq: i = j.
We prove the intermediate claim HiSuccJ: i ∈ ordsucc j.
rewrite the current goal using HijEq (from left to right).
An exact proof term for the current goal is (ordsuccI2 j).
We prove the intermediate claim HcPref: c ∈ Cand_pref j.
We prove the intermediate claim HCprefdef: Cand_pref j = {c0 ∈ Cand|fC c0 ∈ ordsucc j}.
Use reflexivity.
rewrite the current goal using HCprefdef (from left to right).
Apply (SepI Cand (λc0 : set ⇒ fC c0 ∈ ordsucc j) c HcCand) to the current goal.
rewrite the current goal using HfCc (from left to right).
An exact proof term for the current goal is HiSuccJ.
We prove the intermediate claim HclcInFam: closure_of X Tx c ∈ ClCfam j.
An exact proof term for the current goal is (ReplI (Cand_pref j) (λc0 : set ⇒ closure_of X Tx c0) c HcPref).
We prove the intermediate claim HcBasis: c ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ B = Empty) c HcCand).
We prove the intermediate claim HcTx: c ∈ Tx.
An exact proof term for the current goal is (HBasisSubTx c HcBasis).
We prove the intermediate claim HcSubX: c ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx c HTx HcTx).
We prove the intermediate claim Hxclc: x ∈ closure_of X Tx c.
We prove the intermediate claim HcSubCl: c ⊆ closure_of X Tx c.
An exact proof term for the current goal is (subset_of_closure X Tx c HTx HcSubX).
An exact proof term for the current goal is (HcSubCl x Hxc).
We prove the intermediate claim HxClC: x ∈ ClC j.
An exact proof term for the current goal is (UnionI (ClCfam j) x (closure_of X Tx c) Hxclc HclcInFam).
An exact proof term for the current goal is (HxnotClC HxClC).
Assume Hji: j ∈ i.
We prove the intermediate claim HjSuccI: j ∈ ordsucc i.
An exact proof term for the current goal is (ordsuccI1 i j Hji).
We prove the intermediate claim HdPref: d ∈ Dand_pref i.
We prove the intermediate claim HDprefdef: Dand_pref i = {d0 ∈ Dand|fD d0 ∈ ordsucc i}.
Use reflexivity.
rewrite the current goal using HDprefdef (from left to right).
Apply (SepI Dand (λd0 : set ⇒ fD d0 ∈ ordsucc i) d HdDand) to the current goal.
rewrite the current goal using HfDd (from left to right).
An exact proof term for the current goal is HjSuccI.
We prove the intermediate claim HcldInFam: closure_of X Tx d ∈ ClDfam i.
An exact proof term for the current goal is (ReplI (Dand_pref i) (λd0 : set ⇒ closure_of X Tx d0) d HdPref).
We prove the intermediate claim HdBasis: d ∈ Basis.
An exact proof term for the current goal is (SepE1 Basis (λb0 : set ⇒ closure_of X Tx b0 ∩ A = Empty) d HdDand).
We prove the intermediate claim HdTx: d ∈ Tx.
An exact proof term for the current goal is (HBasisSubTx d HdBasis).
We prove the intermediate claim HdSubX: d ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx d HTx HdTx).
We prove the intermediate claim Hxcld: x ∈ closure_of X Tx d.
We prove the intermediate claim HdSubCl: d ⊆ closure_of X Tx d.
An exact proof term for the current goal is (subset_of_closure X Tx d HTx HdSubX).
An exact proof term for the current goal is (HdSubCl x Hxd).
We prove the intermediate claim HxClD: x ∈ ClD i.
An exact proof term for the current goal is (UnionI (ClDfam i) x (closure_of X Tx d) Hxcld HcldInFam).
An exact proof term for the current goal is (HxnotClD HxClD).
∎