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 H0A: 0 ∈ A.
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 (HAsubX 0 H0A).
We prove the intermediate claim H0notB: ¬ (0 ∈ B).
Assume H0B: 0 ∈ B.
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 HVopen_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 HV: X ∖ {0} ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ {0}) HVopen_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 A1 to be the term A ∩ (X ∖ {0}).
We prove the intermediate claim HA1cl: closed_in X Tx A1.
An exact proof term for the current goal is (intersection_of_closed_is_closed X Tx A (X ∖ {0}) HTx HAcl HAX0cl).
Apply (xm (A1 = Empty)) to the current goal.
Assume HA1e: A1 = Empty.
We use {0} to witness the existential quantifier.
We use (X ∖ {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 H0open.
An exact proof term for the current goal is HV.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ {0}.
Apply (xm (a = 0)) to the current goal.
Assume Ha0: a = 0.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is (SingI 0).
Assume Han0: ¬ (a = 0).
Apply FalseE to the current goal.
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 Ha0mem: a ∈ {0}.
We prove the intermediate claim Ha0eq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0mem).
An exact proof term for the current goal is (Han0 Ha0eq).
We prove the intermediate claim HaX0: a ∈ X ∖ {0}.
An exact proof term for the current goal is (setminusI X {0} a HaX HaNot0).
We prove the intermediate claim HaA1: a ∈ A1.
An exact proof term for the current goal is (binintersectI A (X ∖ {0}) a HaA HaX0).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using HA1e (from right to left).
An exact proof term for the current goal is HaA1.
An exact proof term for the current goal is (EmptyE a HaE).
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ X ∖ {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).
We prove the intermediate claim H0B': 0 ∈ B.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is (H0notB H0B').
An exact proof term for the current goal is (setminusI X {0} b HbX Hbnot0).
We will prove {0} ∩ (X ∖ {0}) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {0} ∩ (X ∖ {0}).
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim Hx0: x ∈ {0}.
An exact proof term for the current goal is (binintersectE1 {0} (X ∖ {0}) x Hx).
We prove the intermediate claim HxX0: x ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE2 {0} (X ∖ {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 ∈ {0} ∩ (X ∖ {0}).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HA1nE: ¬ (A1 = Empty).
We prove the intermediate claim HexUB: ∃UB ∈ Tx, B = X ∖ UB.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx B HBcl).
Set UB to be the term Eps_i (λU : set ⇒ U ∈ Tx ∧ B = X ∖ U).
We prove the intermediate claim HUB: UB ∈ Tx ∧ B = X ∖ UB.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ Tx ∧ B = X ∖ U) HexUB).
We prove the intermediate claim HUBTx: UB ∈ Tx.
An exact proof term for the current goal is (andEL (UB ∈ Tx) (B = X ∖ UB) HUB).
We prove the intermediate claim HBdef: B = X ∖ UB.
An exact proof term for the current goal is (andER (UB ∈ Tx) (B = X ∖ UB) HUB).
We prove the intermediate claim HexVA: ∃VA ∈ Tx, A1 = X ∖ VA.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A1 HA1cl).
Set VA to be the term Eps_i (λU : set ⇒ U ∈ Tx ∧ A1 = X ∖ U).
We prove the intermediate claim HVA: VA ∈ Tx ∧ A1 = X ∖ VA.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ U ∈ Tx ∧ A1 = X ∖ U) HexVA).
We prove the intermediate claim HVATx: VA ∈ Tx.
An exact proof term for the current goal is (andEL (VA ∈ Tx) (A1 = X ∖ VA) HVA).
We prove the intermediate claim HA1def: A1 = X ∖ VA.
An exact proof term for the current goal is (andER (VA ∈ Tx) (A1 = X ∖ VA) HVA).
We prove the intermediate claim HA1Bdisj: A1 ∩ B = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ A1 ∩ B.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (binintersectE1 A1 B x Hx).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (binintersectE2 A1 B x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (X ∖ {0}) x HxA1).
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 ∈ A1 ∩ B.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim H0notA1: ¬ (0 ∈ A1).
Assume H0A1: 0 ∈ A1.
We prove the intermediate claim H0X0: 0 ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE2 A (X ∖ {0}) 0 H0A1).
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 H0notB2: ¬ (0 ∈ B).
An exact proof term for the current goal is H0notB.
We prove the intermediate claim HexUV: ∃U1 V1 : set, U1 ∈ Tx ∧ V1 ∈ Tx ∧ A1 ⊆ U1 ∧ B ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (well_ordered_sets_normal_case_nonzero X A1 B UB VA Hwo Hso HTx HA1cl HBcl HA1Bdisj HA1nE HBnE HUBTx HBdef HVATx HA1def H0notA1 H0notB2).
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 HBsub.
Apply Hcore2 to the current goal.
Assume HUV HA1sub.
Apply HUV to the current goal.
Assume HU1 HV1'.
Set V to be the term V1 ∩ (X ∖ {0}).
We prove the intermediate claim HVX0: X ∖ {0} ∈ Tx.
An exact proof term for the current goal is HV.
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx V1 (X ∖ {0}) HTx HV1' HVX0).
Set U to be the term {0} ∪ U1.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (lemma_union_two_open X Tx {0} U1 HTx H0open HU1).
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.
Apply (xm (a = 0)) to the current goal.
Assume Ha0: a = 0.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is (binunionI1 {0} U1 0 (SingI 0)).
Assume Han0: ¬ (a = 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 Ha0mem: a ∈ {0}.
We prove the intermediate claim Ha0eq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0mem).
An exact proof term for the current goal is (Han0 Ha0eq).
We prove the intermediate claim HaX0: a ∈ X ∖ {0}.
An exact proof term for the current goal is (setminusI X {0} a HaX HaNot0).
We prove the intermediate claim HaA1: a ∈ A1.
An exact proof term for the current goal is (binintersectI A (X ∖ {0}) a HaA HaX0).
We prove the intermediate claim HaU1: a ∈ U1.
An exact proof term for the current goal is (HA1sub a HaA1).
An exact proof term for the current goal is (binunionI2 {0} U1 a HaU1).
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
We prove the intermediate claim HbV1: b ∈ V1.
An exact proof term for the current goal is (HBsub b HbB).
We prove the intermediate claim HbX0: b ∈ X ∖ {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).
We prove the intermediate claim H0B': 0 ∈ B.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is (H0notB H0B').
An exact proof term for the current goal is (setminusI X {0} b HbX Hbnot0).
An exact proof term for the current goal is (binintersectI V1 (X ∖ {0}) b HbV1 HbX0).
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 HxV1: x ∈ V1.
An exact proof term for the current goal is (binintersectE1 V1 (X ∖ {0}) x HxV).
We prove the intermediate claim HxX0: x ∈ X ∖ {0}.
An exact proof term for the current goal is (binintersectE2 V1 (X ∖ {0}) x HxV).
Apply (binunionE' {0} U1 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 HxU1: x ∈ U1.
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.
An exact proof term for the current goal is (Hdisj (λU V : set ⇒ x ∈ U) HxUV).
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim HUdef: U = {0} ∪ U1.
Use reflexivity.
rewrite the current goal using HUdef (from right to left).
An exact proof term for the current goal is HxU.
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).
∎