Let X, Tx, A, B, Cand and Dand be given.
Assume HTx: topology_on X Tx.
Assume HAsubX: A ⊆ X.
Assume HBsubX: B ⊆ X.
Assume HCandSubTx: Cand ⊆ Tx.
Assume HDandSubTx: Dand ⊆ Tx.
Assume HCandCount: countable_set Cand.
Assume HDandCount: countable_set Dand.
Assume HAcover: A ⊆ ⋃ Cand.
Assume HBcover: B ⊆ ⋃ Dand.
Assume HCandDisj: ∀c : set, c ∈ Cand → closure_of X Tx c ∩ B = Empty.
Assume HDandDisj: ∀d : set, d ∈ Dand → closure_of X Tx d ∩ A = Empty.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
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 Hd0Tx: d0 ∈ Tx.
An exact proof term for the current goal is (HDandSubTx d0 Hd0Dand).
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 HCeqSubTx: Cand_eq n ⊆ Tx.
An exact proof term for the current goal is (Subq_tra (Cand_eq n) Cand Tx HCeqSubCand HCandSubTx).
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 Hc0Tx: c0 ∈ Tx.
An exact proof term for the current goal is (HCandSubTx c0 Hc0Cand).
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 HDeqSubTx: Dand_eq n ⊆ Tx.
An exact proof term for the current goal is (Subq_tra (Dand_eq n) Dand Tx HDeqSubDand HDandSubTx).
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 (HDandDisj 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 (HCandDisj 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 HcTx: c ∈ Tx.
An exact proof term for the current goal is (HCandSubTx c HcCand).
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 HcTx: c ∈ Tx.
An exact proof term for the current goal is (HCandSubTx c HcCand).
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 HdTx: d ∈ Tx.
An exact proof term for the current goal is (HDandSubTx d HdDand).
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).
∎