Let X and Tx be given.
Assume Hlin: linear_continuum X Tx.
We will prove connected_space X Tx.
Set T0 to be the term (simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y).
Set T1 to be the term T0 ∧ (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y).
Set T2 to be the term T1 ∧ (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = 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 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim Hlub: ∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (andER T1 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = 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 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) HT1).
We prove the intermediate claim Hbetween: ∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y.
An exact proof term for the current goal is (andER T0 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) 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) (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y) 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).
We will prove connected_space X (order_topology X).
We will prove topology_on X (order_topology X) ∧ ¬ (∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ separation_of X U V).
Apply andI to the current goal.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
Assume Hsep: ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ separation_of X U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ separation_of X U V.
Apply HexV to the current goal.
Let V be given.
Assume HUV.
We prove the intermediate claim HUVpair: (U ∈ order_topology X ∧ V ∈ order_topology X) ∧ separation_of X U V.
An exact proof term for the current goal is HUV.
We prove the intermediate claim Hsepof: separation_of X U V.
An exact proof term for the current goal is (andER (U ∈ order_topology X ∧ V ∈ order_topology X) (separation_of X U V) HUVpair).
We prove the intermediate claim H1: ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) Hsepof).
We prove the intermediate claim H2: (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) H1).
We prove the intermediate claim H3: ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty).
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty)) (V ≠ Empty) H1).
We prove the intermediate claim Hpow: U ∈ 𝒫 X ∧ V ∈ 𝒫 X.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) H3).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 X) (V ∈ 𝒫 X) Hpow).
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X) (V ∈ 𝒫 X) Hpow).
We prove the intermediate claim HUVdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) H3).
We prove the intermediate claim Hunion: U ∪ V = X.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) Hsepof).
We prove the intermediate claim HUVopen: U ∈ order_topology X ∧ V ∈ order_topology X.
An exact proof term for the current goal is (andEL (U ∈ order_topology X ∧ V ∈ order_topology X) (separation_of X U V) HUVpair).
We prove the intermediate claim HUopen: U ∈ order_topology X.
An exact proof term for the current goal is (andEL (U ∈ order_topology X) (V ∈ order_topology X) HUVopen).
We prove the intermediate claim HVopen: V ∈ order_topology X.
An exact proof term for the current goal is (andER (U ∈ order_topology X) (V ∈ order_topology X) HUVopen).
Apply (nonempty_has_element U HUne) to the current goal.
Let u0 be given.
Assume Hu0U: u0 ∈ U.
Apply (nonempty_has_element V HVne) to the current goal.
Let v0 be given.
Assume Hv0V: v0 ∈ V.
We prove the intermediate claim Hu0X: u0 ∈ X.
An exact proof term for the current goal is ((PowerE X U HUpow) u0 Hu0U).
We prove the intermediate claim Hv0X: v0 ∈ X.
An exact proof term for the current goal is ((PowerE X V HVpow) v0 Hv0V).
We prove the intermediate claim Hcomp: order_rel X u0 v0 ∨ order_rel X v0 u0.
Apply (order_rel_trichotomy_or_impred X u0 v0 Hso Hu0X Hv0X (order_rel X u0 v0 ∨ order_rel X v0 u0)) to the current goal.
Assume Huv: order_rel X u0 v0.
Apply orIL to the current goal.
An exact proof term for the current goal is Huv.
Assume Heq: u0 = v0.
Apply FalseE to the current goal.
We prove the intermediate claim Huv0: u0 ∈ U ∩ V.
We prove the intermediate claim Hu0V: u0 ∈ V.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hv0V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V).
We prove the intermediate claim HuE: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Huv0.
An exact proof term for the current goal is (EmptyE u0 HuE).
Assume Hvu: order_rel X v0 u0.
Apply orIR to the current goal.
An exact proof term for the current goal is Hvu.
Apply Hcomp to the current goal.
Assume Huv: order_rel X u0 v0.
Set A0 to be the term {x ∈ X|x ∈ U ∧ order_rel X x v0}.
We prove the intermediate claim HA0subX: A0 ⊆ X.
Let x be given.
Assume HxA0: x ∈ A0.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hu0A0: u0 ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) u0 Hu0X) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0U.
An exact proof term for the current goal is Huv.
We prove the intermediate claim HA0ne: A0 ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A0 u0 Hu0A0).
We prove the intermediate claim Hupper: ∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A0 → order_rel X a upper ∨ a = upper.
We use v0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv0X.
Let a be given.
Assume HaA0: a ∈ A0.
We prove the intermediate claim HaConj: a ∈ U ∧ order_rel X a v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) a HaA0).
We prove the intermediate claim Hav0: order_rel X a v0.
An exact proof term for the current goal is (andER (a ∈ U) (order_rel X a v0) HaConj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hav0.
We prove the intermediate claim Hexlub: ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A0 → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A0 → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (Hlub A0 HA0subX HA0ne Hupper).
Apply Hexlub to the current goal.
Let c be given.
Assume Hcpack.
We prove the intermediate claim HcCore: (c ∈ X ∧ (∀a : set, a ∈ A0 → order_rel X a c ∨ a = c)).
An exact proof term for the current goal is (andEL (c ∈ X ∧ (∀a : set, a ∈ A0 → order_rel X a c ∨ a = c)) (∀bound : set, bound ∈ X → (∀a : set, a ∈ A0 → order_rel X a bound ∨ a = bound) → order_rel X c bound ∨ c = bound) Hcpack).
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (andEL (c ∈ X) (∀a : set, a ∈ A0 → order_rel X a c ∨ a = c) HcCore).
We prove the intermediate claim Hcup: ∀a : set, a ∈ A0 → order_rel X a c ∨ a = c.
An exact proof term for the current goal is (andER (c ∈ X) (∀a : set, a ∈ A0 → order_rel X a c ∨ a = c) HcCore).
We prove the intermediate claim Hcleast: ∀bound : set, bound ∈ X → (∀a : set, a ∈ A0 → order_rel X a bound ∨ a = bound) → order_rel X c bound ∨ c = bound.
An exact proof term for the current goal is (andER (c ∈ X ∧ (∀a : set, a ∈ A0 → order_rel X a c ∨ a = c)) (∀bound : set, bound ∈ X → (∀a : set, a ∈ A0 → order_rel X a bound ∨ a = bound) → order_rel X c bound ∨ c = bound) Hcpack).
We prove the intermediate claim HcInUV: c ∈ U ∪ V.
We prove the intermediate claim HcX2: c ∈ X.
An exact proof term for the current goal is HcX.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HcX2.
Apply (binunionE U V c HcInUV) to the current goal.
Assume HcU: c ∈ U.
We prove the intermediate claim Hv0Upper: ∀a : set, a ∈ A0 → order_rel X a v0 ∨ a = v0.
Let a be given.
Assume HaA0: a ∈ A0.
We prove the intermediate claim HaConj: a ∈ U ∧ order_rel X a v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) a HaA0).
We prove the intermediate claim Hav0: order_rel X a v0.
An exact proof term for the current goal is (andER (a ∈ U) (order_rel X a v0) HaConj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hav0.
We prove the intermediate claim HcLeV0: order_rel X c v0 ∨ c = v0.
An exact proof term for the current goal is (Hcleast v0 Hv0X Hv0Upper).
We prove the intermediate claim HcLtV0: order_rel X c v0.
Apply HcLeV0 to the current goal.
Assume Hcv0: order_rel X c v0.
An exact proof term for the current goal is Hcv0.
Assume Hceq: c = v0.
Apply FalseE to the current goal.
We prove the intermediate claim Hv0U: v0 ∈ U.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is HcU.
We prove the intermediate claim Hv0UV: v0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V v0 Hv0U Hv0V).
We prove the intermediate claim Hv0E: v0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hv0UV.
An exact proof term for the current goal is (EmptyE v0 Hv0E).
Set Iv0 to be the term open_ray_lower X v0.
We prove the intermediate claim HIv0B: Iv0 ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X v0 Hv0X).
We prove the intermediate claim HcIv0: c ∈ Iv0.
We prove the intermediate claim HIdef: Iv0 = {x ∈ X|order_rel X x v0}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 v0) c HcX HcLtV0).
We prove the intermediate claim Hexb: ∃b ∈ order_topology_basis X, c ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (order_topology_local_basis_elem X U c Hso HUopen HcU).
Apply Hexb to the current goal.
Let b be given.
Assume HbCore.
Apply HbCore to the current goal.
Assume HbB HbData.
Apply HbData to the current goal.
Assume Hcb HbsubU.
We prove the intermediate claim HBasisOn: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
We prove the intermediate claim Hexb3: ∃b3 ∈ order_topology_basis X, c ∈ b3 ∧ b3 ⊆ b ∩ Iv0.
An exact proof term for the current goal is (basis_on_refine X (order_topology_basis X) HBasisOn b HbB Iv0 HIv0B c Hcb HcIv0).
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3Core.
Apply Hb3Core to the current goal.
Assume Hb3B Hb3Data.
Apply Hb3Data to the current goal.
Assume Hcb3 Hb3Sub.
We prove the intermediate claim Hcases: (∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}) ∨ (∃a ∈ X, b3 = {x ∈ X|order_rel X a x}) ∨ b3 = X.
An exact proof term for the current goal is (order_topology_basis_cases X b3 Hb3B).
Apply Hcases to the current goal.
Assume H123: (((∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})) ∨ (∃a ∈ X, b3 = {x ∈ X|order_rel X a x})).
Apply H123 to the current goal.
Assume H12: ((∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})).
Apply H12 to the current goal.
Assume Hb3I: (∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}).
Apply Hb3I to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim HcInI: c ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hcb3.
We prove the intermediate claim HcProps: order_rel X a c ∧ order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) c HcInI).
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (andER (order_rel X a c) (order_rel X c d) HcProps).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c d HcX HdX Hcd).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hcz: order_rel X c z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim HzI: z ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (order_rel_trans X a c z Hso HaX HcX HzX (andEL (order_rel X a c) (order_rel X c d) HcProps) Hcz).
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzI.
We prove the intermediate claim HzInInter: z ∈ b ∩ Iv0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b Iv0 z HzInInter).
We prove the intermediate claim HzIv0: z ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 b Iv0 z HzInInter).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HbsubU z Hzb).
We prove the intermediate claim Hzltv0: order_rel X z v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) z HzIv0).
We prove the intermediate claim HzA0: z ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzU.
An exact proof term for the current goal is Hzltv0.
Apply (Hcup z HzA0) to the current goal.
Assume Hzltc: order_rel X z c.
We prove the intermediate claim Hcc: order_rel X c c.
An exact proof term for the current goal is (order_rel_trans X c z c Hso HcX HzX HcX Hcz Hzltc).
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hzeq: z = c.
We prove the intermediate claim Hcc: order_rel X c c.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hcz.
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hb3L: (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}).
Apply Hb3L to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim HcInL: c ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hcb3.
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c HcInL).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c d HcX HdX Hcd).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hcz: order_rel X c z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hzld: order_rel X z d.
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzL: z ∈ {x ∈ X|order_rel X x d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) z HzX Hzld).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzL.
We prove the intermediate claim HzInInter: z ∈ b ∩ Iv0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b Iv0 z HzInInter).
We prove the intermediate claim HzIv0: z ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 b Iv0 z HzInInter).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HbsubU z Hzb).
We prove the intermediate claim Hzltv0: order_rel X z v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) z HzIv0).
We prove the intermediate claim HzA0: z ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzU.
An exact proof term for the current goal is Hzltv0.
Apply (Hcup z HzA0) to the current goal.
Assume Hzltc: order_rel X z c.
We prove the intermediate claim Hcc: order_rel X c c.
An exact proof term for the current goal is (order_rel_trans X c z c Hso HcX HzX HcX Hcz Hzltc).
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hzeq: z = c.
We prove the intermediate claim Hcc: order_rel X c c.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hcz.
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hb3R: (∃a ∈ X, b3 = {x ∈ X|order_rel X a x}).
Apply Hb3R to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX Hb3eq.
We prove the intermediate claim HcInR: c ∈ {x ∈ X|order_rel X a x}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hcb3.
We prove the intermediate claim Hac: order_rel X a c.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) c HcInR).
We prove the intermediate claim Hav0: order_rel X a v0.
An exact proof term for the current goal is (order_rel_trans X a c v0 Hso HaX HcX Hv0X Hac HcLtV0).
We prove the intermediate claim Hv0b3: v0 ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) v0 Hv0X Hav0).
We prove the intermediate claim Hv0InInter: v0 ∈ b ∩ Iv0.
An exact proof term for the current goal is (Hb3Sub v0 Hv0b3).
We prove the intermediate claim Hv0Iv0: v0 ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 b Iv0 v0 Hv0InInter).
We prove the intermediate claim Hv0ltv0: order_rel X v0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) v0 Hv0Iv0).
An exact proof term for the current goal is ((order_rel_irref X v0) Hv0ltv0).
Assume Hb3X: b3 = X.
We prove the intermediate claim Hv0b3: v0 ∈ b3.
rewrite the current goal using Hb3X (from left to right).
An exact proof term for the current goal is Hv0X.
We prove the intermediate claim Hv0InInter: v0 ∈ b ∩ Iv0.
An exact proof term for the current goal is (Hb3Sub v0 Hv0b3).
We prove the intermediate claim Hv0Iv0: v0 ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 b Iv0 v0 Hv0InInter).
We prove the intermediate claim Hv0ltv0: order_rel X v0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) v0 Hv0Iv0).
An exact proof term for the current goal is ((order_rel_irref X v0) Hv0ltv0).
Assume HcV: c ∈ V.
We prove the intermediate claim HcnotU: ¬ (c ∈ U).
Assume HcU2: c ∈ U.
We prove the intermediate claim HcUV: c ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V c HcU2 HcV).
We prove the intermediate claim HcE: c ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HcUV.
An exact proof term for the current goal is (EmptyE c HcE).
We prove the intermediate claim Hcup_lt: ∀a : set, a ∈ A0 → order_rel X a c.
Let a be given.
Assume HaA0: a ∈ A0.
Apply (Hcup a HaA0) to the current goal.
Assume Hac: order_rel X a c.
An exact proof term for the current goal is Hac.
Assume Haeq: a = c.
Apply FalseE to the current goal.
We prove the intermediate claim HcA0: c ∈ A0.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HaA0.
We prove the intermediate claim HcConj: c ∈ U ∧ order_rel X c v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) c HcA0).
We prove the intermediate claim HcU2: c ∈ U.
An exact proof term for the current goal is (andEL (c ∈ U) (order_rel X c v0) HcConj).
An exact proof term for the current goal is (HcnotU HcU2).
We prove the intermediate claim HexbV: ∃b ∈ order_topology_basis X, c ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (order_topology_local_basis_elem X V c Hso HVopen HcV).
Apply HexbV to the current goal.
Let b be given.
Assume HbCore.
Apply HbCore to the current goal.
Assume HbB HbData.
Apply HbData to the current goal.
Assume Hcb HbsubV.
We prove the intermediate claim Hcasesb: (∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d}) ∨ (∃a ∈ X, b = {x ∈ X|order_rel X a x}) ∨ b = X.
An exact proof term for the current goal is (order_topology_basis_cases X b HbB).
Apply Hcasesb to the current goal.
Assume H123b: (((∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d})) ∨ (∃a ∈ X, b = {x ∈ X|order_rel X a x})).
Apply H123b to the current goal.
Assume H12b: ((∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d})).
Apply H12b to the current goal.
Assume HbI: (∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}).
Apply HbI to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hbeq.
We prove the intermediate claim HcInI: c ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim HcProps: order_rel X a c ∧ order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) c HcInI).
We prove the intermediate claim Hac: order_rel X a c.
An exact proof term for the current goal is (andEL (order_rel X a c) (order_rel X c d) HcProps).
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (andER (order_rel X a c) (order_rel X c d) HcProps).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A0 → order_rel X x a ∨ x = a).
Assume Hub: ∀x : set, x ∈ A0 → order_rel X x a ∨ x = a.
We prove the intermediate claim Hca: order_rel X c a ∨ c = a.
An exact proof term for the current goal is (Hcleast a HaX Hub).
Apply Hca to the current goal.
Assume HcaRel: order_rel X c a.
We prove the intermediate claim Haa: order_rel X a a.
An exact proof term for the current goal is (order_rel_trans X a c a Hso HaX HcX HaX Hac HcaRel).
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
Assume Hceq: c = a.
We prove the intermediate claim Haa: order_rel X a a.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hac.
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A0 → order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A0 → order_rel X x a ∨ x = a) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A0 → order_rel X x a ∨ x = a).
We prove the intermediate claim HxA0_and: x ∈ A0 ∧ ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_imp (x ∈ A0) (order_rel X x a ∨ x = a) HnotImp).
We prove the intermediate claim HxA0: x ∈ A0.
An exact proof term for the current goal is (andEL (x ∈ A0) (¬ (order_rel X x a ∨ x = a)) HxA0_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (andER (x ∈ A0) (¬ (order_rel X x a ∨ x = a)) HxA0_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a) ∧ x ≠ a.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a) (x = a) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a.
An exact proof term for the current goal is (andER (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hxa: order_rel X a x.
Apply (order_rel_trichotomy_or_impred X a x Hso HaX HxX (order_rel X a x)) to the current goal.
Assume Hax: order_rel X a x.
An exact proof term for the current goal is Hax.
Assume Heq: a = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxc: order_rel X x c.
An exact proof term for the current goal is (Hcup_lt x HxA0).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c d Hso HxX HcX HdX Hxc Hcd).
We prove the intermediate claim HxI: x ∈ {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxa.
An exact proof term for the current goal is Hxd.
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HxI.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HbsubV x Hxb).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (order_rel X x v0) (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbL: (∃d ∈ X, b = {x ∈ X|order_rel X x d}).
Apply HbL to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hbeq.
We prove the intermediate claim HcInL: c ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c HcInL).
We prove the intermediate claim HxA0: ∃x : set, x ∈ A0.
We use u0 to witness the existential quantifier.
An exact proof term for the current goal is Hu0A0.
Apply HxA0 to the current goal.
Let x be given.
Assume HxA0w: x ∈ A0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0w).
We prove the intermediate claim Hxc: order_rel X x c.
An exact proof term for the current goal is (Hcup_lt x HxA0w).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c d Hso HxX HcX HdX Hxc Hcd).
We prove the intermediate claim HxL: x ∈ {x0 ∈ X|order_rel X x0 d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) x HxX Hxd).
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HxL.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HbsubV x Hxb).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (order_rel X x v0) (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0w)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbR: (∃a ∈ X, b = {x ∈ X|order_rel X a x}).
Apply HbR to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX Hbeq.
We prove the intermediate claim HcInR: c ∈ {x ∈ X|order_rel X a x}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim Hac: order_rel X a c.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) c HcInR).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A0 → order_rel X x a ∨ x = a).
Assume Hub: ∀x : set, x ∈ A0 → order_rel X x a ∨ x = a.
We prove the intermediate claim Hca: order_rel X c a ∨ c = a.
An exact proof term for the current goal is (Hcleast a HaX Hub).
Apply Hca to the current goal.
Assume HcaRel: order_rel X c a.
We prove the intermediate claim Haa: order_rel X a a.
An exact proof term for the current goal is (order_rel_trans X a c a Hso HaX HcX HaX Hac HcaRel).
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
Assume Hceq: c = a.
We prove the intermediate claim Haa: order_rel X a a.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hac.
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A0 → order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A0 → order_rel X x a ∨ x = a) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A0 → order_rel X x a ∨ x = a).
We prove the intermediate claim HxA0_and: x ∈ A0 ∧ ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_imp (x ∈ A0) (order_rel X x a ∨ x = a) HnotImp).
We prove the intermediate claim HxA0: x ∈ A0.
An exact proof term for the current goal is (andEL (x ∈ A0) (¬ (order_rel X x a ∨ x = a)) HxA0_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (andER (x ∈ A0) (¬ (order_rel X x a ∨ x = a)) HxA0_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a) ∧ x ≠ a.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a) (x = a) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a.
An exact proof term for the current goal is (andER (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hxa: order_rel X a x.
Apply (order_rel_trichotomy_or_impred X a x Hso HaX HxX (order_rel X a x)) to the current goal.
Assume Hax: order_rel X a x.
An exact proof term for the current goal is Hax.
Assume Heq: a = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) x HxX Hxa).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HbsubV x Hxb).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (order_rel X x v0) (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbX: b = X.
We prove the intermediate claim Hu0V2: u0 ∈ V.
Apply HbsubV to the current goal.
rewrite the current goal using HbX (from left to right).
An exact proof term for the current goal is Hu0X.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V2).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Assume Hvu: order_rel X v0 u0.
Set A1 to be the term {x ∈ X|x ∈ V ∧ order_rel X x u0}.
We prove the intermediate claim HA1subX: A1 ⊆ X.
Let x be given.
Assume HxA1: x ∈ A1.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hv0A1: v0 ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) v0 Hv0X) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hv0V.
An exact proof term for the current goal is Hvu.
We prove the intermediate claim HA1ne: A1 ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A1 v0 Hv0A1).
We prove the intermediate claim Hupper1: ∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A1 → order_rel X a upper ∨ a = upper.
We use u0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0X.
Let a be given.
Assume HaA1: a ∈ A1.
We prove the intermediate claim HaConj: a ∈ V ∧ order_rel X a u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) a HaA1).
We prove the intermediate claim Hau0: order_rel X a u0.
An exact proof term for the current goal is (andER (a ∈ V) (order_rel X a u0) HaConj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hexlub1: ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A1 → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A1 → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (Hlub A1 HA1subX HA1ne Hupper1).
Apply Hexlub1 to the current goal.
Let c1 be given.
Assume Hc1pack.
We prove the intermediate claim Hc1Core: (c1 ∈ X ∧ (∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1)).
An exact proof term for the current goal is (andEL (c1 ∈ X ∧ (∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1)) (∀bound : set, bound ∈ X → (∀a : set, a ∈ A1 → order_rel X a bound ∨ a = bound) → order_rel X c1 bound ∨ c1 = bound) Hc1pack).
We prove the intermediate claim Hc1X: c1 ∈ X.
An exact proof term for the current goal is (andEL (c1 ∈ X) (∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1) Hc1Core).
We prove the intermediate claim Hcup1: ∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1.
An exact proof term for the current goal is (andER (c1 ∈ X) (∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1) Hc1Core).
We prove the intermediate claim Hcleast1: ∀bound : set, bound ∈ X → (∀a : set, a ∈ A1 → order_rel X a bound ∨ a = bound) → order_rel X c1 bound ∨ c1 = bound.
An exact proof term for the current goal is (andER (c1 ∈ X ∧ (∀a : set, a ∈ A1 → order_rel X a c1 ∨ a = c1)) (∀bound : set, bound ∈ X → (∀a : set, a ∈ A1 → order_rel X a bound ∨ a = bound) → order_rel X c1 bound ∨ c1 = bound) Hc1pack).
We prove the intermediate claim Hc1InUV: c1 ∈ U ∪ V.
We prove the intermediate claim Hc1X2: c1 ∈ X.
An exact proof term for the current goal is Hc1X.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is Hc1X2.
Apply (binunionE U V c1 Hc1InUV) to the current goal.
Assume Hc1U: c1 ∈ U.
We prove the intermediate claim Hc1notV: ¬ (c1 ∈ V).
Assume Hc1V2: c1 ∈ V.
We prove the intermediate claim Hc1UV: c1 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V c1 Hc1U Hc1V2).
We prove the intermediate claim Hc1E: c1 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hc1UV.
An exact proof term for the current goal is (EmptyE c1 Hc1E).
We prove the intermediate claim Hcup1_lt: ∀a : set, a ∈ A1 → order_rel X a c1.
Let a be given.
Assume HaA1: a ∈ A1.
Apply (Hcup1 a HaA1) to the current goal.
Assume Hac: order_rel X a c1.
An exact proof term for the current goal is Hac.
Assume Haeq: a = c1.
Apply FalseE to the current goal.
We prove the intermediate claim Hc1A1: c1 ∈ A1.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is HaA1.
We prove the intermediate claim Hc1Conj: c1 ∈ V ∧ order_rel X c1 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) c1 Hc1A1).
We prove the intermediate claim Hc1V2: c1 ∈ V.
An exact proof term for the current goal is (andEL (c1 ∈ V) (order_rel X c1 u0) Hc1Conj).
An exact proof term for the current goal is (Hc1notV Hc1V2).
We prove the intermediate claim HexbU: ∃b ∈ order_topology_basis X, c1 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (order_topology_local_basis_elem X U c1 Hso HUopen Hc1U).
Apply HexbU to the current goal.
Let b be given.
Assume HbCore.
Apply HbCore to the current goal.
Assume HbB HbData.
Apply HbData to the current goal.
Assume Hcb HbsubU.
We prove the intermediate claim Hcasesb: (∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d}) ∨ (∃a ∈ X, b = {x ∈ X|order_rel X a x}) ∨ b = X.
An exact proof term for the current goal is (order_topology_basis_cases X b HbB).
Apply Hcasesb to the current goal.
Assume H123b: (((∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d})) ∨ (∃a ∈ X, b = {x ∈ X|order_rel X a x})).
Apply H123b to the current goal.
Assume H12b: ((∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b = {x ∈ X|order_rel X x d})).
Apply H12b to the current goal.
Assume HbI: (∃a ∈ X, ∃d ∈ X, b = {x ∈ X|order_rel X a x ∧ order_rel X x d}).
Apply HbI to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hbeq.
We prove the intermediate claim Hc1InI: c1 ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim Hc1Props: order_rel X a c1 ∧ order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) c1 Hc1InI).
We prove the intermediate claim Hac1: order_rel X a c1.
An exact proof term for the current goal is (andEL (order_rel X a c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (andER (order_rel X a c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A1 → order_rel X x a ∨ x = a).
Assume Hub: ∀x : set, x ∈ A1 → order_rel X x a ∨ x = a.
We prove the intermediate claim Hca: order_rel X c1 a ∨ c1 = a.
An exact proof term for the current goal is (Hcleast1 a HaX Hub).
Apply Hca to the current goal.
Assume HcaRel: order_rel X c1 a.
We prove the intermediate claim Haa: order_rel X a a.
An exact proof term for the current goal is (order_rel_trans X a c1 a Hso HaX Hc1X HaX Hac1 HcaRel).
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
Assume Hceq: c1 = a.
We prove the intermediate claim Haa: order_rel X a a.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hac1.
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A1 → order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A1 → order_rel X x a ∨ x = a) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A1 → order_rel X x a ∨ x = a).
We prove the intermediate claim HxA1_and: x ∈ A1 ∧ ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_imp (x ∈ A1) (order_rel X x a ∨ x = a) HnotImp).
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (andEL (x ∈ A1) (¬ (order_rel X x a ∨ x = a)) HxA1_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (andER (x ∈ A1) (¬ (order_rel X x a ∨ x = a)) HxA1_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a) ∧ x ≠ a.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a) (x = a) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a.
An exact proof term for the current goal is (andER (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hxa: order_rel X a x.
Apply (order_rel_trichotomy_or_impred X a x Hso HaX HxX (order_rel X a x)) to the current goal.
Assume Hax: order_rel X a x.
An exact proof term for the current goal is Hax.
Assume Heq: a = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxc1: order_rel X x c1.
An exact proof term for the current goal is (Hcup1_lt x HxA1).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c1 d Hso HxX Hc1X HdX Hxc1 Hc1d).
We prove the intermediate claim HxI: x ∈ {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxa.
An exact proof term for the current goal is Hxd.
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HxI.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HbsubU x Hxb).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (order_rel X x u0) (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbL: (∃d ∈ X, b = {x ∈ X|order_rel X x d}).
Apply HbL to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hbeq.
We prove the intermediate claim Hc1InL: c1 ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c1 Hc1InL).
Set x to be the term v0.
We prove the intermediate claim HxA1w: x ∈ A1.
An exact proof term for the current goal is Hv0A1.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1w).
We prove the intermediate claim Hxc1: order_rel X x c1.
An exact proof term for the current goal is (Hcup1_lt x HxA1w).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c1 d Hso HxX Hc1X HdX Hxc1 Hc1d).
We prove the intermediate claim HxL: x ∈ {x0 ∈ X|order_rel X x0 d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) x HxX Hxd).
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HxL.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HbsubU x Hxb).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is Hv0V.
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbR: (∃a ∈ X, b = {x ∈ X|order_rel X a x}).
Apply HbR to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX Hbeq.
We prove the intermediate claim Hc1InR: c1 ∈ {x ∈ X|order_rel X a x}.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hcb.
We prove the intermediate claim Hac1: order_rel X a c1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) c1 Hc1InR).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A1 → order_rel X x a ∨ x = a).
Assume Hub: ∀x : set, x ∈ A1 → order_rel X x a ∨ x = a.
We prove the intermediate claim Hca: order_rel X c1 a ∨ c1 = a.
An exact proof term for the current goal is (Hcleast1 a HaX Hub).
Apply Hca to the current goal.
Assume HcaRel: order_rel X c1 a.
We prove the intermediate claim Haa: order_rel X a a.
An exact proof term for the current goal is (order_rel_trans X a c1 a Hso HaX Hc1X HaX Hac1 HcaRel).
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
Assume Hceq: c1 = a.
We prove the intermediate claim Haa: order_rel X a a.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hac1.
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A1 → order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A1 → order_rel X x a ∨ x = a) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A1 → order_rel X x a ∨ x = a).
We prove the intermediate claim HxA1_and: x ∈ A1 ∧ ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (not_imp (x ∈ A1) (order_rel X x a ∨ x = a) HnotImp).
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (andEL (x ∈ A1) (¬ (order_rel X x a ∨ x = a)) HxA1_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a ∨ x = a).
An exact proof term for the current goal is (andER (x ∈ A1) (¬ (order_rel X x a ∨ x = a)) HxA1_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a) ∧ x ≠ a.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a) (x = a) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a.
An exact proof term for the current goal is (andER (¬ (order_rel X x a)) (¬ (x = a)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hxa: order_rel X a x.
Apply (order_rel_trichotomy_or_impred X a x Hso HaX HxX (order_rel X a x)) to the current goal.
Assume Hax: order_rel X a x.
An exact proof term for the current goal is Hax.
Assume Heq: a = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxb: x ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) x HxX Hxa).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HbsubU x Hxb).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (order_rel X x u0) (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (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).
Assume HbX: b = X.
We prove the intermediate claim Hv0U2: v0 ∈ U.
Apply HbsubU to the current goal.
rewrite the current goal using HbX (from left to right).
An exact proof term for the current goal is Hv0X.
We prove the intermediate claim Hv0UV: v0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V v0 Hv0U2 Hv0V).
We prove the intermediate claim Hv0E: v0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hv0UV.
An exact proof term for the current goal is (EmptyE v0 Hv0E).
Assume Hc1V: c1 ∈ V.
We prove the intermediate claim Hu0Upper1: ∀a : set, a ∈ A1 → order_rel X a u0 ∨ a = u0.
Let a be given.
Assume HaA1: a ∈ A1.
We prove the intermediate claim HaConj: a ∈ V ∧ order_rel X a u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) a HaA1).
We prove the intermediate claim Hau0: order_rel X a u0.
An exact proof term for the current goal is (andER (a ∈ V) (order_rel X a u0) HaConj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hc1LeU0: order_rel X c1 u0 ∨ c1 = u0.
An exact proof term for the current goal is (Hcleast1 u0 Hu0X Hu0Upper1).
We prove the intermediate claim Hc1LtU0: order_rel X c1 u0.
Apply Hc1LeU0 to the current goal.
Assume Hcu0: order_rel X c1 u0.
An exact proof term for the current goal is Hcu0.
Assume Hceq: c1 = u0.
Apply FalseE to the current goal.
We prove the intermediate claim Hu0V2: u0 ∈ V.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hc1V.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V2).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Set Iu0 to be the term open_ray_lower X u0.
We prove the intermediate claim HIu0B: Iu0 ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X u0 Hu0X).
We prove the intermediate claim Hc1Iu0: c1 ∈ Iu0.
We prove the intermediate claim HIdef: Iu0 = {x ∈ X|order_rel X x u0}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 u0) c1 Hc1X Hc1LtU0).
We prove the intermediate claim Hexb: ∃b ∈ order_topology_basis X, c1 ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (order_topology_local_basis_elem X V c1 Hso HVopen Hc1V).
Apply Hexb to the current goal.
Let b be given.
Assume HbCore.
Apply HbCore to the current goal.
Assume HbB HbData.
Apply HbData to the current goal.
Assume Hc1b HbsubV.
We prove the intermediate claim HBasisOn: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
We prove the intermediate claim Hexb3: ∃b3 ∈ order_topology_basis X, c1 ∈ b3 ∧ b3 ⊆ b ∩ Iu0.
An exact proof term for the current goal is (basis_on_refine X (order_topology_basis X) HBasisOn b HbB Iu0 HIu0B c1 Hc1b Hc1Iu0).
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3Core.
Apply Hb3Core to the current goal.
Assume Hb3B Hb3Data.
Apply Hb3Data to the current goal.
Assume Hc1b3 Hb3Sub.
We prove the intermediate claim Hcases: (∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}) ∨ (∃a ∈ X, b3 = {x ∈ X|order_rel X a x}) ∨ b3 = X.
An exact proof term for the current goal is (order_topology_basis_cases X b3 Hb3B).
Apply Hcases to the current goal.
Assume H123: (((∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})) ∨ (∃a ∈ X, b3 = {x ∈ X|order_rel X a x})).
Apply H123 to the current goal.
Assume H12: ((∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})).
Apply H12 to the current goal.
Assume Hb3I: (∃a ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a x ∧ order_rel X x d}).
Apply Hb3I to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim Hc1InI: c1 ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Hc1Props: order_rel X a c1 ∧ order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) c1 Hc1InI).
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (andER (order_rel X a c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c1 z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c1 d Hc1X HdX Hc1d).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c1 z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hc1z: order_rel X c1 z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim HzI: z ∈ {x ∈ X|order_rel X a x ∧ order_rel X x d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 d) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (order_rel_trans X a c1 z Hso HaX Hc1X HzX (andEL (order_rel X a c1) (order_rel X c1 d) Hc1Props) Hc1z).
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzI.
We prove the intermediate claim HzInInter: z ∈ b ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b Iu0 z HzInInter).
We prove the intermediate claim HzIu0: z ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b Iu0 z HzInInter).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (HbsubV z Hzb).
We prove the intermediate claim Hzltu0: order_rel X z u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) z HzIu0).
We prove the intermediate claim HzA1: z ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzV.
An exact proof term for the current goal is Hzltu0.
Apply (Hcup1 z HzA1) to the current goal.
Assume Hzltc1: order_rel X z c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
An exact proof term for the current goal is (order_rel_trans X c1 z c1 Hso Hc1X HzX Hc1X Hc1z Hzltc1).
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hzeq: z = c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hc1z.
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hb3L: (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}).
Apply Hb3L to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim Hc1InL: c1 ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c1 Hc1InL).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c1 z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c1 d Hc1X HdX Hc1d).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c1 z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hc1z: order_rel X c1 z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hzld: order_rel X z d.
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzL: z ∈ {x ∈ X|order_rel X x d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) z HzX Hzld).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzL.
We prove the intermediate claim HzInInter: z ∈ b ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b Iu0 z HzInInter).
We prove the intermediate claim HzIu0: z ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b Iu0 z HzInInter).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (HbsubV z Hzb).
We prove the intermediate claim Hzltu0: order_rel X z u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) z HzIu0).
We prove the intermediate claim HzA1: z ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzV.
An exact proof term for the current goal is Hzltu0.
Apply (Hcup1 z HzA1) to the current goal.
Assume Hzltc1: order_rel X z c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
An exact proof term for the current goal is (order_rel_trans X c1 z c1 Hso Hc1X HzX Hc1X Hc1z Hzltc1).
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hzeq: z = c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hc1z.
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hb3R: (∃a ∈ X, b3 = {x ∈ X|order_rel X a x}).
Apply Hb3R to the current goal.
Let a be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume HaX Hb3eq.
We prove the intermediate claim Hc1InR: c1 ∈ {x ∈ X|order_rel X a x}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Hac1: order_rel X a c1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) c1 Hc1InR).
We prove the intermediate claim Hau0: order_rel X a u0.
An exact proof term for the current goal is (order_rel_trans X a c1 u0 Hso HaX Hc1X Hu0X Hac1 Hc1LtU0).
We prove the intermediate claim Hu0b3: u0 ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) u0 Hu0X Hau0).
We prove the intermediate claim Hu0InInter: u0 ∈ b ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub u0 Hu0b3).
We prove the intermediate claim Hu0Iu0: u0 ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b Iu0 u0 Hu0InInter).
We prove the intermediate claim Hu0ltu0: order_rel X u0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) u0 Hu0Iu0).
An exact proof term for the current goal is ((order_rel_irref X u0) Hu0ltu0).
Assume Hb3X: b3 = X.
We prove the intermediate claim Hu0b3: u0 ∈ b3.
rewrite the current goal using Hb3X (from left to right).
An exact proof term for the current goal is Hu0X.
We prove the intermediate claim Hu0InInter: u0 ∈ b ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub u0 Hu0b3).
We prove the intermediate claim Hu0Iu0: u0 ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b Iu0 u0 Hu0InInter).
We prove the intermediate claim Hu0ltu0: order_rel X u0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) u0 Hu0Iu0).
An exact proof term for the current goal is ((order_rel_irref X u0) Hu0ltu0).
∎