Let X, A and B be given.
Assume Hwo: well_ordered_set X.
Assume Hso: simply_ordered_set X.
Assume HAcl: closed_in X (order_topology X) A.
Assume HBcl: closed_in X (order_topology X) B.
Assume HABdisj: A ∩ B = Empty.
Assume HAnE: A ≠ Empty.
Assume HBnE: B ≠ Empty.
Assume H0B: 0 ∈ B.
We will prove ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Set Tx to be the term order_topology X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
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 H0X: 0 ∈ X.
An exact proof term for the current goal is (HBsubX 0 H0B).
We prove the intermediate claim H0notA: ¬ (0 ∈ A).
Assume H0A: 0 ∈ A.
We prove the intermediate claim H0AB: 0 ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B 0 H0A H0B).
We prove the intermediate claim H0E: 0 ∈ Empty.
An exact proof term for the current goal is (HABdisj (λU V : set ⇒ 0 ∈ U) H0AB).
An exact proof term for the current goal is (EmptyE 0 H0E).
We prove the intermediate claim H0open: {0} ∈ Tx.
An exact proof term for the current goal is (singleton0_open_in_order_topology_well_ordered_nonempty X Hwo Hso H0X).
We prove the intermediate claim Hcl0: closed_in X Tx {0}.
We prove the intermediate claim HH: Hausdorff_space X Tx.
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx 0 HH H0X).
We prove the intermediate claim HUopen_in: open_in X Tx (X ∖ {0}).
An exact proof term for the current goal is (open_of_closed_complement X Tx {0} Hcl0).
We prove the intermediate claim HUc: X ∖ {0} ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ {0}) HUopen_in).
We prove the intermediate claim HAX0cl: closed_in X Tx (X ∖ {0}).
An exact proof term for the current goal is (closed_of_open_complement X Tx {0} HTx H0open).
Set B1 to be the term B ∩ (X ∖ {0}).
We prove the intermediate claim HB1cl: closed_in X Tx B1.
An exact proof term for the current goal is (intersection_of_closed_is_closed X Tx B (X ∖ {0}) HTx HBcl HAX0cl).
Apply (xm (B1 = Empty)) to the current goal.
Assume HB1e: B1 = Empty.
We use (X ∖ {0}) to witness the existential quantifier.
We use {0} to witness the existential quantifier.
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 HUc.
An exact proof term for the current goal is H0open.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ X ∖ {0}.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim Hanot0: ¬ (a ∈ {0}).
Assume Ha0: a ∈ {0}.
We prove the intermediate claim Haeq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0).
We prove the intermediate claim H0A': 0 ∈ A.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is (H0notA H0A').
An exact proof term for the current goal is (setminusI X {0} a HaX Hanot0).
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ {0}.
Apply (xm (b = 0)) to the current goal.
Assume Hb0: b = 0.
rewrite the current goal using Hb0 (from left to right).
An exact proof term for the current goal is (SingI 0).
Assume Hbn0: ¬ (b = 0).
Apply FalseE to the current goal.
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim Hbnot0: ¬ (b ∈ {0}).
Assume Hb0: b ∈ {0}.
We prove the intermediate claim Hbeq: b = 0.
An exact proof term for the current goal is (SingE 0 b Hb0).
An exact proof term for the current goal is (Hbn0 Hbeq).
We prove the intermediate claim HbX0: b ∈ X ∖ {0}.
An exact proof term for the current goal is (setminusI X {0} b HbX Hbnot0).
We prove the intermediate claim HbB1: b ∈ B1.
An exact proof term for the current goal is (binintersectI B (X ∖ {0}) b HbB HbX0).
We prove the intermediate claim HbE: b ∈ Empty.
rewrite the current goal using HB1e (from right to left).
An exact proof term for the current goal is HbB1.
An exact proof term for the current goal is (EmptyE b HbE).
We will prove (X ∖ {0}) ∩ {0} = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ {0}) ∩ {0}.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxX0: x ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE1 (X ∖ {0}) {0} x Hx).
We prove the intermediate claim Hx0: x ∈ {0}.
An exact proof term for the current goal is (binintersectE2 (X ∖ {0}) {0} x Hx).
An exact proof term for the current goal is ((setminusE2 X {0} x HxX0) Hx0).
Let x be given.
Assume HxE: x ∈ Empty.
We will prove x ∈ (X ∖ {0}) ∩ {0}.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HB1nE: ¬ (B1 = Empty).
We prove the intermediate claim HexUA: ∃UA ∈ Tx, A = X ∖ UA.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
Set UA to be the term Eps_i (λU : set ⇒ U ∈ Tx ∧ A = X ∖ U).
We prove the intermediate claim HUA: UA ∈ Tx ∧ A = X ∖ UA.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ Tx ∧ A = X ∖ U) HexUA).
We prove the intermediate claim HUATx: UA ∈ Tx.
An exact proof term for the current goal is (andEL (UA ∈ Tx) (A = X ∖ UA) HUA).
We prove the intermediate claim HAdef: A = X ∖ UA.
An exact proof term for the current goal is (andER (UA ∈ Tx) (A = X ∖ UA) HUA).
We prove the intermediate claim HexVB: ∃VB ∈ Tx, B1 = X ∖ VB.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx B1 HB1cl).
Set VB to be the term Eps_i (λU : set ⇒ U ∈ Tx ∧ B1 = X ∖ U).
We prove the intermediate claim HVB: VB ∈ Tx ∧ B1 = X ∖ VB.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ Tx ∧ B1 = X ∖ U) HexVB).
We prove the intermediate claim HVBTx: VB ∈ Tx.
An exact proof term for the current goal is (andEL (VB ∈ Tx) (B1 = X ∖ VB) HVB).
We prove the intermediate claim HB1def: B1 = X ∖ VB.
An exact proof term for the current goal is (andER (VB ∈ Tx) (B1 = X ∖ VB) HVB).
We prove the intermediate claim HAB1disj: A ∩ B1 = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ A ∩ B1.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A B1 x Hx).
We prove the intermediate claim HxB1: x ∈ B1.
An exact proof term for the current goal is (binintersectE2 A B1 x Hx).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (binintersectE1 B (X ∖ {0}) x HxB1).
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.
An exact proof term for the current goal is (HABdisj (λU V : set ⇒ x ∈ U) HxAB).
An exact proof term for the current goal is (EmptyE x HxE).
Let x be given.
Assume HxE: x ∈ Empty.
We will prove x ∈ A ∩ B1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim H0notB1: ¬ (0 ∈ B1).
Assume H0B1: 0 ∈ B1.
We prove the intermediate claim H0X0: 0 ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE2 B (X ∖ {0}) 0 H0B1).
We prove the intermediate claim H00: 0 ∈ {0}.
An exact proof term for the current goal is (SingI 0).
An exact proof term for the current goal is ((setminusE2 X {0} 0 H0X0) H00).
We prove the intermediate claim H0notA2: ¬ (0 ∈ A).
An exact proof term for the current goal is H0notA.
We prove the intermediate claim HexUV: ∃U1 V1 : set, U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ B1 ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (well_ordered_sets_normal_case_nonzero X A B1 VB UA Hwo Hso HTx HAcl HB1cl HAB1disj HAnE HB1nE HVBTx HB1def HUATx HAdef H0notA2 H0notB1).
Apply HexUV to the current goal.
Let U1 be given.
Assume HU1core.
Apply HU1core to the current goal.
Let V1 be given.
Assume HV1core.
Apply HV1core to the current goal.
Assume Hcore Hdisj.
Apply Hcore to the current goal.
Assume Hcore2 HB1sub.
Apply Hcore2 to the current goal.
Assume HUV HAsub.
Apply HUV to the current goal.
Assume HU1 HV1'.
Set U to be the term U1 ∩ (X ∖ {0}).
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U1 (X ∖ {0}) HTx HU1 HUc).
Set V to be the term {0} ∪ V1.
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (lemma_union_two_open X Tx {0} V1 HTx H0open HV1').
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = 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 HU.
An exact proof term for the current goal is HV.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ U.
We prove the intermediate claim HaU1: a ∈ U1.
An exact proof term for the current goal is (HAsub a HaA).
We prove the intermediate claim HaX0: a ∈ X ∖ {0}.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim Hanot0: ¬ (a ∈ {0}).
Assume Ha0: a ∈ {0}.
We prove the intermediate claim Haeq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0).
We prove the intermediate claim H0A': 0 ∈ A.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is (H0notA H0A').
An exact proof term for the current goal is (setminusI X {0} a HaX Hanot0).
An exact proof term for the current goal is (binintersectI U1 (X ∖ {0}) a HaU1 HaX0).
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
Apply (xm (b = 0)) to the current goal.
Assume Hb0: b = 0.
rewrite the current goal using Hb0 (from left to right).
An exact proof term for the current goal is (binunionI1 {0} V1 0 (SingI 0)).
Assume Hbn0: ¬ (b = 0).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim Hbnot0: ¬ (b ∈ {0}).
Assume Hb0: b ∈ {0}.
We prove the intermediate claim Hbeq: b = 0.
An exact proof term for the current goal is (SingE 0 b Hb0).
An exact proof term for the current goal is (Hbn0 Hbeq).
We prove the intermediate claim HbX0: b ∈ X ∖ {0}.
An exact proof term for the current goal is (setminusI X {0} b HbX Hbnot0).
We prove the intermediate claim HbB1: b ∈ B1.
An exact proof term for the current goal is (binintersectI B (X ∖ {0}) b HbB HbX0).
We prove the intermediate claim HbV1: b ∈ V1.
An exact proof term for the current goal is (HB1sub b HbB1).
An exact proof term for the current goal is (binunionI2 {0} V1 b HbV1).
We will prove U ∩ V = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∩ V.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x Hx).
We prove the intermediate claim HxX0: x ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE2 U1 (X ∖ {0}) x HxU).
Apply (binunionE' {0} V1 x False) to the current goal.
Assume Hx0: x ∈ {0}.
An exact proof term for the current goal is ((setminusE2 X {0} x HxX0) Hx0).
Assume HxV1: x ∈ V1.
We prove the intermediate claim HxU1: x ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 (X ∖ {0}) x HxU).
We prove the intermediate claim HxUV: x ∈ U1 ∩ V1.
An exact proof term for the current goal is (binintersectI U1 V1 x HxU1 HxV1).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim HVdef: V = {0} ∪ V1.
Use reflexivity.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HxV.
Let x be given.
Assume HxE: x ∈ Empty.
We will prove x ∈ U ∩ V.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
∎