Let X, Tx, A, B, S, Ts, WF, C and pick be given.
Assume Hlin: linear_continuum X Tx.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume HAB: A ∩ B = Empty.
Assume HSdef: S = X βˆ– (A βˆͺ B).
Assume HTsdef: Ts = subspace_topology X Tx S.
Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Assume HCdef: C = {pick W0|W0 ∈ WF}.
Assume Hpick: βˆ€W : set, W ∈ WF β†’ pick W ∈ W.
Set T0 to be the term (simply_ordered_set X ∧ Tx = order_topology X) ∧ (βˆƒx0 y0 : set, x0 ∈ X ∧ y0 ∈ X ∧ x0 β‰  y0).
Set T1 to be the term T0 ∧ (βˆ€x0 y0 : set, x0 ∈ X β†’ y0 ∈ X β†’ order_rel X x0 y0 β†’ βˆƒz0 : set, z0 ∈ X ∧ order_rel X x0 z0 ∧ order_rel X z0 y0).
Set T2 to be the term T1 ∧ (βˆ€A0 : set, A0 βŠ† X β†’ A0 β‰  Empty β†’ (βˆƒupper : set, upper ∈ X ∧ βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 upper ∨ a0 = upper) β†’ βˆƒlub : set, lub ∈ X ∧ (βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 lub ∨ a0 = lub) ∧ (βˆ€bound : set, bound ∈ X β†’ (βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 bound ∨ a0 = bound) β†’ order_rel X lub bound ∨ lub = bound)).
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is Hlin.
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (βˆ€A0 : set, A0 βŠ† X β†’ A0 β‰  Empty β†’ (βˆƒupper : set, upper ∈ X ∧ βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 upper ∨ a0 = upper) β†’ βˆƒlub : set, lub ∈ X ∧ (βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 lub ∨ a0 = lub) ∧ (βˆ€bound : set, bound ∈ X β†’ (βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 bound ∨ a0 = bound) β†’ order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim HT0: T0.
An exact proof term for the current goal is (andEL T0 (βˆ€x0 y0 : set, x0 ∈ X β†’ y0 ∈ X β†’ order_rel X x0 y0 β†’ βˆƒz0 : set, z0 ∈ X ∧ order_rel X x0 z0 ∧ order_rel X z0 y0) HT1).
We prove the intermediate claim HsoEq: simply_ordered_set X ∧ Tx = order_topology X.
An exact proof term for the current goal is (andEL (simply_ordered_set X ∧ Tx = order_topology X) (βˆƒx0 y0 : set, x0 ∈ X ∧ y0 ∈ X ∧ x0 β‰  y0) HT0).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is (andEL (simply_ordered_set X) (Tx = order_topology X) HsoEq).
We prove the intermediate claim HTxeq: Tx = order_topology X.
An exact proof term for the current goal is (andER (simply_ordered_set X) (Tx = order_topology X) HsoEq).
rewrite the current goal using HTxeq (from left to right).
Set U to be the term X βˆ– C.
We will prove U ∈ order_topology X.
We prove the intermediate claim Hord: order_topology X = generated_topology X (order_topology_basis X).
Use reflexivity.
rewrite the current goal using Hord (from left to right).
We prove the intermediate claim Hgen: generated_topology X (order_topology_basis X) = {U0 ∈ 𝒫 X|βˆ€x0 ∈ U0, βˆƒb0 ∈ order_topology_basis X, x0 ∈ b0 ∧ b0 βŠ† U0}.
Use reflexivity.
rewrite the current goal using Hgen (from left to right).
Apply SepI to the current goal.
We prove the intermediate claim HUsubX: U βŠ† X.
An exact proof term for the current goal is (setminus_Subq X C).
An exact proof term for the current goal is (PowerI X U HUsubX).
Let x be given.
Assume HxU: x ∈ U.
We will prove βˆƒb ∈ order_topology_basis X, x ∈ b ∧ b βŠ† U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X C x HxU).
Apply (xm (x ∈ S)) to the current goal.
Assume HxS: x ∈ S.
We prove the intermediate claim HTx: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HTsEq: Ts = subspace_topology X (order_topology X) S.
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is HTsdef.
We prove the intermediate claim HSsubX: S βŠ† X.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (setminus_Subq X (A βˆͺ B)).
We prove the intermediate claim HTs: topology_on S Ts.
rewrite the current goal using HTsEq (from left to right).
An exact proof term for the current goal is (subspace_topology_is_topology X (order_topology X) S HTx HSsubX).
We prove the intermediate claim HABcl: closed_in X (order_topology X) A.
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is HAcl.
We prove the intermediate claim HBBcl: closed_in X (order_topology X) B.
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is HBcl.
We prove the intermediate claim HunionCl: closed_in X (order_topology X) (A βˆͺ B).
An exact proof term for the current goal is (union_of_closed_is_closed X (order_topology X) A B HTx HABcl HBBcl).
We prove the intermediate claim HSopenIn: open_in X (order_topology X) S.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (open_of_closed_complement X (order_topology X) (A βˆͺ B) HunionCl).
We prove the intermediate claim HSopen: S ∈ order_topology X.
An exact proof term for the current goal is (open_in_elem X (order_topology X) S HSopenIn).
We prove the intermediate claim HlocX: locally_connected X (order_topology X).
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is (linear_continuum_locally_connected X Tx Hlin).
We prove the intermediate claim HlocS: locally_connected S Ts.
rewrite the current goal using HTsEq (from left to right).
An exact proof term for the current goal is (open_subspace_locally_connected X (order_topology X) S HlocX HSopen).
Set W to be the term component_of S Ts x.
We prove the intermediate claim HWdef0: W = component_of S Ts x.
Use reflexivity.
We prove the intermediate claim HWopenInS: open_in S Ts W.
An exact proof term for the current goal is (components_are_open_in_locally_connected S Ts HlocS x HxS).
We prove the intermediate claim HWTs: W ∈ Ts.
An exact proof term for the current goal is (open_in_elem S Ts W HWopenInS).
We prove the intermediate claim HWTs': W ∈ subspace_topology X (order_topology X) S.
rewrite the current goal using HTsEq (from right to left).
An exact proof term for the current goal is HWTs.
We prove the intermediate claim HexV: βˆƒV ∈ order_topology X, W = V ∩ S.
An exact proof term for the current goal is (subspace_topologyE X (order_topology X) S W HWTs').
Apply HexV to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ order_topology X.
An exact proof term for the current goal is (andEL (V ∈ order_topology X) (W = V ∩ S) HVpair).
We prove the intermediate claim HWV: W = V ∩ S.
An exact proof term for the current goal is (andER (V ∈ order_topology X) (W = V ∩ S) HVpair).
We prove the intermediate claim HWTx: W ∈ order_topology X.
rewrite the current goal using HWV (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X (order_topology X) V S HTx HVTx HSopen).
Apply (xm (W ∈ WF)) to the current goal.
Assume HWinWF: W ∈ WF.
We prove the intermediate claim HxNotC: x βˆ‰ C.
An exact proof term for the current goal is (setminusE2 X C x HxU).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HpickW: pick W ∈ W.
An exact proof term for the current goal is (Hpick W HWinWF).
We prove the intermediate claim HpickC: pick W ∈ C.
rewrite the current goal using HCdef (from left to right).
An exact proof term for the current goal is (ReplI WF (Ξ»W0 : set β‡’ pick W0) W HWinWF).
We prove the intermediate claim Hneqxc: x β‰  pick W.
Assume Heq: x = pick W.
Apply HxNotC to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpickC.
We prove the intermediate claim HH: Hausdorff_space X (order_topology X).
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
We prove the intermediate claim HpickComp: pick W ∈ component_of S Ts x.
rewrite the current goal using HWdef0 (from right to left).
An exact proof term for the current goal is HpickW.
We prove the intermediate claim HpickS: pick W ∈ S.
An exact proof term for the current goal is (SepE1 S (Ξ»y0 : set β‡’ βˆƒD : set, connected_space D (subspace_topology S Ts D) ∧ x ∈ D ∧ y0 ∈ D) (pick W) HpickComp).
We prove the intermediate claim HpickX: pick W ∈ X.
An exact proof term for the current goal is (HSsubX (pick W) HpickS).
We prove the intermediate claim HexSep: βˆƒU1 U2 : set, U1 ∈ order_topology X ∧ U2 ∈ order_topology X ∧ x ∈ U1 ∧ pick W ∈ U2 ∧ U1 ∩ U2 = Empty.
An exact proof term for the current goal is (Hausdorff_space_separation X (order_topology X) x (pick W) HH HxX HpickX Hneqxc).
Apply HexSep to the current goal.
Let U1 be given.
Assume HU1pack.
Apply HU1pack to the current goal.
Let U2 be given.
Assume HU1U2: U1 ∈ order_topology X ∧ U2 ∈ order_topology X ∧ x ∈ U1 ∧ pick W ∈ U2 ∧ U1 ∩ U2 = Empty.
Set P12 to be the term U1 ∈ order_topology X ∧ U2 ∈ order_topology X.
Set P3 to be the term x ∈ U1.
Set P4 to be the term pick W ∈ U2.
Set P5 to be the term U1 ∩ U2 = Empty.
We prove the intermediate claim Hleft1: (P12 ∧ P3) ∧ P4.
An exact proof term for the current goal is (andEL ((P12 ∧ P3) ∧ P4) P5 HU1U2).
We prove the intermediate claim HU1U2Empty: P5.
An exact proof term for the current goal is (andER ((P12 ∧ P3) ∧ P4) P5 HU1U2).
We prove the intermediate claim Hleft2: P12 ∧ P3.
An exact proof term for the current goal is (andEL (P12 ∧ P3) P4 Hleft1).
We prove the intermediate claim HpickU2: P4.
An exact proof term for the current goal is (andER (P12 ∧ P3) P4 Hleft1).
We prove the intermediate claim HU1U2InT: P12.
An exact proof term for the current goal is (andEL P12 P3 Hleft2).
We prove the intermediate claim HxU1: P3.
An exact proof term for the current goal is (andER P12 P3 Hleft2).
We prove the intermediate claim HU1Tx: U1 ∈ order_topology X.
An exact proof term for the current goal is (andEL (U1 ∈ order_topology X) (U2 ∈ order_topology X) HU1U2InT).
We prove the intermediate claim HU2Tx: U2 ∈ order_topology X.
An exact proof term for the current goal is (andER (U1 ∈ order_topology X) (U2 ∈ order_topology X) HU1U2InT).
Set N to be the term U1 ∩ W.
We prove the intermediate claim HNopen: N ∈ order_topology X.
An exact proof term for the current goal is (topology_binintersect_closed X (order_topology X) U1 W HTx HU1Tx HWTx).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (binintersectI U1 W x HxU1 HxW).
We prove the intermediate claim HpickNotU1: pick W βˆ‰ U1.
Assume Hpin: pick W ∈ U1.
We prove the intermediate claim HpinInt: pick W ∈ U1 ∩ U2.
An exact proof term for the current goal is (binintersectI U1 U2 (pick W) Hpin HpickU2).
We prove the intermediate claim HpinE: pick W ∈ Empty.
rewrite the current goal using HU1U2Empty (from right to left).
An exact proof term for the current goal is HpinInt.
An exact proof term for the current goal is (EmptyE (pick W) HpinE False).
We prove the intermediate claim HpickNotN: pick W βˆ‰ N.
Assume Hpn: pick W ∈ N.
We prove the intermediate claim HpnU1: pick W ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 W (pick W) Hpn).
An exact proof term for the current goal is (HpickNotU1 HpnU1).
We prove the intermediate claim HNgen: N ∈ generated_topology X (order_topology_basis X).
rewrite the current goal using Hord (from right to left).
An exact proof term for the current goal is HNopen.
We prove the intermediate claim HNmem: N ∈ {U0 ∈ 𝒫 X|βˆ€y0 ∈ U0, βˆƒb0 ∈ order_topology_basis X, y0 ∈ b0 ∧ b0 βŠ† U0}.
rewrite the current goal using Hgen (from right to left).
An exact proof term for the current goal is HNgen.
We prove the intermediate claim HNprop: βˆ€y0 ∈ N, βˆƒb0 ∈ order_topology_basis X, y0 ∈ b0 ∧ b0 βŠ† N.
An exact proof term for the current goal is (SepE2 (𝒫 X) (Ξ»U0 : set β‡’ βˆ€y0 ∈ U0, βˆƒb0 ∈ order_topology_basis X, y0 ∈ b0 ∧ b0 βŠ† U0) N HNmem).
We prove the intermediate claim HexbN: βˆƒb ∈ order_topology_basis X, x ∈ b ∧ b βŠ† N.
An exact proof term for the current goal is (HNprop x HxN).
Apply HexbN to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ order_topology_basis X.
An exact proof term for the current goal is (andEL (b ∈ order_topology_basis X) (x ∈ b ∧ b βŠ† N) Hbpair).
We prove the intermediate claim Hbrest: x ∈ b ∧ b βŠ† N.
An exact proof term for the current goal is (andER (b ∈ order_topology_basis X) (x ∈ b ∧ b βŠ† N) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b βŠ† N) Hbrest).
We prove the intermediate claim HbsubN: b βŠ† N.
An exact proof term for the current goal is (andER (x ∈ b) (b βŠ† N) Hbrest).
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HNsubU: N βŠ† U.
Let y be given.
Assume HyN: y ∈ N.
We will prove y ∈ U.
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (binintersectE2 U1 W y HyN).
We prove the intermediate claim HyX: y ∈ X.
We prove the intermediate claim HyVS: y ∈ V ∩ S.
rewrite the current goal using HWV (from right to left).
An exact proof term for the current goal is HyW.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (binintersectE2 V S y HyVS).
An exact proof term for the current goal is (HSsubX y HyS).
We prove the intermediate claim HyNotC: y βˆ‰ C.
Assume HyC: y ∈ C.
We prove the intermediate claim HCW1: C ∩ W = {pick W}.
An exact proof term for the current goal is (ex32_8b_C_intersection_W X A B S Ts WF C pick HTs HWFdef HCdef Hpick W HWinWF).
We prove the intermediate claim HyCW: y ∈ C ∩ W.
An exact proof term for the current goal is (binintersectI C W y HyC HyW).
We prove the intermediate claim HySing: y ∈ {pick W}.
rewrite the current goal using HCW1 (from right to left).
An exact proof term for the current goal is HyCW.
We prove the intermediate claim HyEq: y = pick W.
An exact proof term for the current goal is (SingE (pick W) y HySing).
We prove the intermediate claim Hpn: pick W ∈ N.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is HyN.
An exact proof term for the current goal is (HpickNotN Hpn).
An exact proof term for the current goal is (setminusI X C y HyX HyNotC).
An exact proof term for the current goal is (Subq_tra b N U HbsubN HNsubU).
Assume HWnotWF: ¬ (W ∈ WF).
We prove the intermediate claim HCW: C ∩ W = Empty.
An exact proof term for the current goal is (ex32_8b_component_disjoint_C_if_not_in_WF X A B S Ts WF C pick HTs HWFdef HCdef Hpick x HxS W HWdef0 HWnotWF).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (point_in_component S Ts x HTs HxS).
We prove the intermediate claim HWprop: βˆ€y ∈ W, βˆƒb ∈ order_topology_basis X, y ∈ b ∧ b βŠ† W.
An exact proof term for the current goal is (SepE2 (𝒫 X) (Ξ»U0 : set β‡’ βˆ€y0 ∈ U0, βˆƒb0 ∈ order_topology_basis X, y0 ∈ b0 ∧ b0 βŠ† U0) W HWTx).
We prove the intermediate claim HexbW: βˆƒb ∈ order_topology_basis X, x ∈ b ∧ b βŠ† W.
An exact proof term for the current goal is (HWprop x HxW).
Apply HexbW to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ order_topology_basis X.
An exact proof term for the current goal is (andEL (b ∈ order_topology_basis X) (x ∈ b ∧ b βŠ† W) Hbpair).
We prove the intermediate claim Hbrest: x ∈ b ∧ b βŠ† W.
An exact proof term for the current goal is (andER (b ∈ order_topology_basis X) (x ∈ b ∧ b βŠ† W) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b βŠ† W) Hbrest).
We prove the intermediate claim HbsubW: b βŠ† W.
An exact proof term for the current goal is (andER (x ∈ b) (b βŠ† W) Hbrest).
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HWsubU: W βŠ† U.
Let y be given.
Assume HyW: y ∈ W.
We will prove y ∈ U.
We prove the intermediate claim HyVS: y ∈ V ∩ S.
rewrite the current goal using HWV (from right to left).
An exact proof term for the current goal is HyW.
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (binintersectE2 V S y HyVS).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HSsubX y HyS).
We prove the intermediate claim HyNotC: y βˆ‰ C.
Assume HyC: y ∈ C.
We prove the intermediate claim HyCW: y ∈ C ∩ W.
An exact proof term for the current goal is (binintersectI C W y HyC HyW).
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using HCW (from right to left).
An exact proof term for the current goal is HyCW.
An exact proof term for the current goal is (EmptyE y HyE False).
An exact proof term for the current goal is (setminusI X C y HyX HyNotC).
An exact proof term for the current goal is (Subq_tra b W U HbsubW HWsubU).
Assume HxNotS: ¬ (x ∈ S).
We prove the intermediate claim HxAB: x ∈ (A βˆͺ B).
Apply (xm (x ∈ (A βˆͺ B))) to the current goal.
Assume HxAB0: x ∈ (A βˆͺ B).
An exact proof term for the current goal is HxAB0.
Assume HxNotAB: Β¬ (x ∈ (A βˆͺ B)).
We prove the intermediate claim HxS': x ∈ S.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (setminusI X (A βˆͺ B) x HxX HxNotAB).
An exact proof term for the current goal is (HxNotS HxS' (x ∈ (A βˆͺ B))).
Apply (binunionE A B x HxAB) to the current goal.
Assume HxA: x ∈ A.
The rest of this subproof is missing.
Assume HxB: x ∈ B.
The rest of this subproof is missing.
∎