Let X and Y be given.
Assume Hso: simply_ordered_set X.
Assume Hconv: convex_in X Y.
We will prove order_topology_inherited X Y = subspace_topology X (order_topology X) Y.
Set Binh to be the term order_topology_basis_inherited X Y.
Set Tx to be the term order_topology X.
Set Tsub to be the term subspace_topology X Tx Y.
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 HYsub: Y ⊆ X.
An exact proof term for the current goal is (convex_in_subset X Y Hconv).
We prove the intermediate claim HtopSub: topology_on Y Tsub.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
We prove the intermediate claim HBsub: ∀b ∈ Binh, b ∈ Tsub.
Let b be given.
Assume Hb: b ∈ Binh.
Set A to be the term {I ∈ 𝒫 Y|∃a ∈ Y, ∃b0 ∈ Y, I = {x ∈ Y|order_rel X a x ∧ order_rel X x b0}}.
Set B to be the term {I ∈ 𝒫 Y|∃b0 ∈ Y, I = {x ∈ Y|order_rel X x b0}}.
Set C to be the term {I ∈ 𝒫 Y|∃a ∈ Y, I = {x ∈ Y|order_rel X a x}}.
Set Bold to be the term (A ∪ B ∪ C).
We prove the intermediate claim HbIn: b ∈ (Bold ∪ {Y}).
We prove the intermediate claim Hdef: Binh = (Bold ∪ {Y}).
Use reflexivity.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is Hb.
Apply (binunionE' Bold {Y} b (b ∈ Tsub)) to the current goal.
Assume HbBold: b ∈ Bold.
Apply (binunionE' (A ∪ B) C b (b ∈ Tsub)) to the current goal.
Assume HbAB: b ∈ (A ∪ B).
Apply (binunionE' A B b (b ∈ Tsub)) to the current goal.
Assume HbA: b ∈ A.
We prove the intermediate claim Hex: ∃a ∈ Y, ∃b0 ∈ Y, b = {x ∈ Y|order_rel X a x ∧ order_rel X x b0}.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λI : set ⇒ ∃a ∈ Y, ∃b0 ∈ Y, I = {x ∈ Y|order_rel X a x ∧ order_rel X x b0}) b HbA).
Apply Hex to the current goal.
Let a be given.
Assume HaPair.
Apply HaPair to the current goal.
Assume HaY: a ∈ Y.
Assume Hexb0.
Apply Hexb0 to the current goal.
Let b1 be given.
Assume Hb1Pair.
Apply Hb1Pair to the current goal.
Assume Hb1Y: b1 ∈ Y.
Assume Hbeq: b = {x ∈ Y|order_rel X a x ∧ order_rel X x b1}.
Set V to be the term {x ∈ X|order_rel X a x ∧ order_rel X x b1}.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HYsub a HaY).
We prove the intermediate claim Hb1X: b1 ∈ X.
An exact proof term for the current goal is (HYsub b1 Hb1Y).
We prove the intermediate claim HVbasis: V ∈ order_topology_basis X.
Set A0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}}.
Set B0 to be the term {I ∈ 𝒫 X|∃b0 ∈ X, I = {x0 ∈ X|order_rel X x0 b0}}.
Set C0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}}.
Set Bold0 to be the term (A0 ∪ B0 ∪ C0).
We prove the intermediate claim HVinA0: V ∈ A0.
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
Apply PowerI X V to the current goal.
Let x be given.
Assume HxV: x ∈ V.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxV).
We prove the intermediate claim Hex0: ∃a0 ∈ X, ∃b0 ∈ X, V = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaX.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1X.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, ∃b0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}) V HVpow Hex0).
We prove the intermediate claim HVinBold0: V ∈ Bold0.
An exact proof term for the current goal is (binunionI1 (A0 ∪ B0) C0 V (binunionI1 A0 B0 V HVinA0)).
We prove the intermediate claim HVin: V ∈ (Bold0 ∪ {X}).
An exact proof term for the current goal is (binunionI1 Bold0 {X} V HVinBold0).
We prove the intermediate claim Hdef: order_topology_basis X = (Bold0 ∪ {X}).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is HVin.
We prove the intermediate claim HBBasis: 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 HVgen: V ∈ generated_topology X (order_topology_basis X).
An exact proof term for the current goal is (generated_topology_contains_basis X (order_topology_basis X) HBBasis V HVbasis).
We prove the intermediate claim HVTx: V ∈ Tx.
We prove the intermediate claim HdefTx: Tx = generated_topology X (order_topology_basis X).
Use reflexivity.
rewrite the current goal using HdefTx (from left to right).
An exact proof term for the current goal is HVgen.
We prove the intermediate claim HbVY: b = V ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume HxB: x ∈ b.
We prove the intermediate claim HxBdef: x ∈ {x0 ∈ Y|order_rel X a x0 ∧ order_rel X x0 b1}.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is HxB.
We prove the intermediate claim HxProp: order_rel X a x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 Y (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxBdef).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxBdef).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HYsub x HxY).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxX HxProp).
An exact proof term for the current goal is (binintersectI V Y x HxV HxY).
Let x be given.
Assume HxVY: x ∈ V ∩ Y.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
We prove the intermediate claim HxProp: order_rel X a x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxV).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b1) x HxY HxProp).
rewrite the current goal using HbVY (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVTx).
Assume HbB: b ∈ B.
We prove the intermediate claim Hex: ∃b0 ∈ Y, b = {x ∈ Y|order_rel X x b0}.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λI : set ⇒ ∃b0 ∈ Y, I = {x ∈ Y|order_rel X x b0}) b HbB).
Apply Hex to the current goal.
Let b0 be given.
Assume Hb0Pair.
Apply Hb0Pair to the current goal.
Assume Hb0Y: b0 ∈ Y.
Assume Hbeq: b = {x ∈ Y|order_rel X x b0}.
Set V to be the term {x ∈ X|order_rel X x b0}.
We prove the intermediate claim Hb0X: b0 ∈ X.
An exact proof term for the current goal is (HYsub b0 Hb0Y).
We prove the intermediate claim HVbasis: V ∈ order_topology_basis X.
Set A0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b1 ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1}}.
Set B0 to be the term {I ∈ 𝒫 X|∃b1 ∈ X, I = {x0 ∈ X|order_rel X x0 b1}}.
Set C0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}}.
Set Bold0 to be the term (A0 ∪ B0 ∪ C0).
We prove the intermediate claim HVinB0: V ∈ B0.
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
Apply PowerI X V to the current goal.
Let x be given.
Assume HxV: x ∈ V.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X x0 b0) x HxV).
We prove the intermediate claim Hex0: ∃b1 ∈ X, V = {x0 ∈ X|order_rel X x0 b1}.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0X.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λI : set ⇒ ∃b1 ∈ X, I = {x0 ∈ X|order_rel X x0 b1}) V HVpow Hex0).
We prove the intermediate claim HVinBold0: V ∈ Bold0.
An exact proof term for the current goal is (binunionI1 (A0 ∪ B0) C0 V (binunionI2 A0 B0 V HVinB0)).
We prove the intermediate claim HVin: V ∈ (Bold0 ∪ {X}).
An exact proof term for the current goal is (binunionI1 Bold0 {X} V HVinBold0).
We prove the intermediate claim Hdef: order_topology_basis X = (Bold0 ∪ {X}).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is HVin.
We prove the intermediate claim HBBasis: 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 HVgen: V ∈ generated_topology X (order_topology_basis X).
An exact proof term for the current goal is (generated_topology_contains_basis X (order_topology_basis X) HBBasis V HVbasis).
We prove the intermediate claim HVTx: V ∈ Tx.
We prove the intermediate claim HdefTx: Tx = generated_topology X (order_topology_basis X).
Use reflexivity.
rewrite the current goal using HdefTx (from left to right).
An exact proof term for the current goal is HVgen.
We prove the intermediate claim HbVY: b = V ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume HxB: x ∈ b.
We prove the intermediate claim HxY: x ∈ Y.
We prove the intermediate claim HxBdef: x ∈ {x0 ∈ Y|order_rel X x0 b0}.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is HxB.
An exact proof term for the current goal is (SepE1 Y (λx0 : set ⇒ order_rel X x0 b0) x HxBdef).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HYsub x HxY).
We prove the intermediate claim HxProp: order_rel X x b0.
We prove the intermediate claim HxBdef: x ∈ {x0 ∈ Y|order_rel X x0 b0}.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is HxB.
An exact proof term for the current goal is (SepE2 Y (λx0 : set ⇒ order_rel X x0 b0) x HxBdef).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b0) x HxX HxProp).
An exact proof term for the current goal is (binintersectI V Y x HxV HxY).
Let x be given.
Assume HxVY: x ∈ V ∩ Y.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
We prove the intermediate claim HxProp: order_rel X x b0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 b0) x HxV).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel X x0 b0) x HxY HxProp).
rewrite the current goal using HbVY (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVTx).
An exact proof term for the current goal is HbAB.
Assume HbC: b ∈ C.
We prove the intermediate claim Hex: ∃a ∈ Y, b = {x ∈ Y|order_rel X a x}.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λI : set ⇒ ∃a ∈ Y, I = {x ∈ Y|order_rel X a x}) b HbC).
Apply Hex to the current goal.
Let a be given.
Assume HaPair.
Apply HaPair to the current goal.
Assume HaY: a ∈ Y.
Assume Hbeq: b = {x ∈ Y|order_rel X a x}.
Set V to be the term {x ∈ X|order_rel X a x}.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HYsub a HaY).
We prove the intermediate claim HVbasis: V ∈ order_topology_basis X.
Set A0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}}.
Set B0 to be the term {I ∈ 𝒫 X|∃b0 ∈ X, I = {x0 ∈ X|order_rel X x0 b0}}.
Set C0 to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}}.
Set Bold0 to be the term (A0 ∪ B0 ∪ C0).
We prove the intermediate claim HVinC0: V ∈ C0.
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
Apply PowerI X V to the current goal.
Let x be given.
Assume HxV: x ∈ V.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0) x HxV).
We prove the intermediate claim Hex0: ∃a0 ∈ X, V = {x0 ∈ X|order_rel X a0 x0}.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaX.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}) V HVpow Hex0).
We prove the intermediate claim HVinBold0: V ∈ Bold0.
An exact proof term for the current goal is (binunionI2 (A0 ∪ B0) C0 V HVinC0).
We prove the intermediate claim HVin: V ∈ (Bold0 ∪ {X}).
An exact proof term for the current goal is (binunionI1 Bold0 {X} V HVinBold0).
We prove the intermediate claim Hdef: order_topology_basis X = (Bold0 ∪ {X}).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is HVin.
We prove the intermediate claim HBBasis: 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 HVgen: V ∈ generated_topology X (order_topology_basis X).
An exact proof term for the current goal is (generated_topology_contains_basis X (order_topology_basis X) HBBasis V HVbasis).
We prove the intermediate claim HVTx: V ∈ Tx.
We prove the intermediate claim HdefTx: Tx = generated_topology X (order_topology_basis X).
Use reflexivity.
rewrite the current goal using HdefTx (from left to right).
An exact proof term for the current goal is HVgen.
We prove the intermediate claim HbVY: b = V ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume HxB: x ∈ b.
We prove the intermediate claim HxY: x ∈ Y.
We prove the intermediate claim HxBdef: x ∈ {x0 ∈ Y|order_rel X a x0}.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is HxB.
An exact proof term for the current goal is (SepE1 Y (λx0 : set ⇒ order_rel X a x0) x HxBdef).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HYsub x HxY).
We prove the intermediate claim HxProp: order_rel X a x.
We prove the intermediate claim HxBdef: x ∈ {x0 ∈ Y|order_rel X a x0}.
rewrite the current goal using Hbeq (from right to left) at position 1.
An exact proof term for the current goal is HxB.
An exact proof term for the current goal is (SepE2 Y (λx0 : set ⇒ order_rel X a x0) x HxBdef).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) x HxX HxProp).
An exact proof term for the current goal is (binintersectI V Y x HxV HxY).
Let x be given.
Assume HxVY: x ∈ V ∩ Y.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
We prove the intermediate claim HxProp: order_rel X a x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) x HxV).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel X a x0) x HxY HxProp).
rewrite the current goal using HbVY (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVTx).
An exact proof term for the current goal is HbBold.
Assume HbY: b ∈ {Y}.
We prove the intermediate claim Hbeq: b = Y.
An exact proof term for the current goal is (SingE Y b HbY).
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HXYeq: X ∩ Y = Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 X Y).
Let y be given.
Assume Hy: y ∈ Y.
An exact proof term for the current goal is (binintersectI X Y y (HYsub y Hy) Hy).
We prove the intermediate claim HXYin: (X ∩ Y) ∈ Tsub.
An exact proof term for the current goal is (subspace_topologyI X Tx Y X HXTx).
rewrite the current goal using HXYeq (from right to left) at position 1.
An exact proof term for the current goal is HXYin.
An exact proof term for the current goal is HbIn.
We prove the intermediate claim Hfiner: finer_than Tsub (generated_topology Y Binh).
An exact proof term for the current goal is (generated_topology_finer_weak Y Binh Tsub HtopSub HBsub).
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ order_topology_inherited X Y.
We will prove U ∈ Tsub.
An exact proof term for the current goal is (Hfiner U HU).
Let U be given.
Assume HU: U ∈ Tsub.
We will prove U ∈ order_topology_inherited X Y.
We will prove U ∈ generated_topology Y Binh.
We prove the intermediate claim HgenDef: generated_topology Y Binh = {U0 ∈ 𝒫 Y|∀x0 ∈ U0, ∃b0 ∈ Binh, x0 ∈ b0 ∧ b0 ⊆ U0}.
Use reflexivity.
rewrite the current goal using HgenDef (from left to right).
We prove the intermediate claim HUpow: U ∈ 𝒫 Y.
An exact proof term for the current goal is (subspace_topology_in_Power X Tx Y U HU).
Apply (SepI (𝒫 Y) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ Binh, x0 ∈ b0 ∧ b0 ⊆ U0) U) to the current goal.
An exact proof term for the current goal is HUpow.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HUrep: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).
Apply HUrep to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HxVY: x ∈ V ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
We prove the intermediate claim HdefTx: Tx = generated_topology X (order_topology_basis X).
Use reflexivity.
We prove the intermediate claim HVgen: V ∈ generated_topology X (order_topology_basis X).
rewrite the current goal using HdefTx (from right to left).
An exact proof term for the current goal is HVTx.
We prove the intermediate claim HVloc: ∀x0 ∈ V, ∃b0 ∈ order_topology_basis X, x0 ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x1 ∈ U0, ∃b1 ∈ order_topology_basis X, x1 ∈ b1 ∧ b1 ⊆ U0) V HVgen).
We prove the intermediate claim Hexb: ∃b0 ∈ order_topology_basis X, x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (HVloc x HxV).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B: b0 ∈ order_topology_basis X.
An exact proof term for the current goal is (andEL (b0 ∈ order_topology_basis X) (x ∈ b0 ∧ b0 ⊆ V) Hb0pair).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (andER (b0 ∈ order_topology_basis X) (x ∈ b0 ∧ b0 ⊆ V) Hb0pair).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ V) Hb0prop).
We prove the intermediate claim Hb0subV: b0 ⊆ V.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ V) Hb0prop).
Set bY to be the term b0 ∩ Y.
We use bY to witness the existential quantifier.
Apply andI to the current goal.
Set Ainh to be the term {I ∈ 𝒫 Y|∃a ∈ Y, ∃b1 ∈ Y, I = {z ∈ Y|order_rel X a z ∧ order_rel X z b1}}.
Set Binh_ray to be the term {I ∈ 𝒫 Y|∃b1 ∈ Y, I = {z ∈ Y|order_rel X z b1}}.
Set Cinh_ray to be the term {I ∈ 𝒫 Y|∃a ∈ Y, I = {z ∈ Y|order_rel X a z}}.
Set Boldinh to be the term (Ainh ∪ Binh_ray ∪ Cinh_ray).
Set A0 to be the term {I ∈ 𝒫 X|∃a ∈ X, ∃b1 ∈ X, I = {z ∈ X|order_rel X a z ∧ order_rel X z b1}}.
Set B0 to be the term {I ∈ 𝒫 X|∃b1 ∈ X, I = {z ∈ X|order_rel X z b1}}.
Set C0 to be the term {I ∈ 𝒫 X|∃a ∈ X, I = {z ∈ X|order_rel X a z}}.
Set Bold0 to be the term (A0 ∪ B0 ∪ C0).
Apply (binunionE Bold0 {X} b0 Hb0B) to the current goal.
Assume Hb0Bold: b0 ∈ Bold0.
Apply (binunionE (A0 ∪ B0) C0 b0 Hb0Bold) to the current goal.
Assume Hb0AB: b0 ∈ (A0 ∪ B0).
Apply (binunionE A0 B0 b0 Hb0AB) to the current goal.
Assume Hb0A0: b0 ∈ A0.
We prove the intermediate claim HexInt: ∃a0 ∈ X, ∃b1 ∈ X, b0 = {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, ∃b1 ∈ X, I = {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}) b0 Hb0A0).
Apply HexInt to the current goal.
Let a0 be given.
Assume Ha0pair.
Apply Ha0pair to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hexb1.
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hb1pair.
Apply Hb1pair to the current goal.
Assume Hb1X: b1 ∈ X.
Assume Hb0eq: b0 = {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
We prove the intermediate claim HbYdef: bY = {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 b0 Y z Hz).
We prove the intermediate claim HzIn: z ∈ {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hzb0.
We prove the intermediate claim HzProp: order_rel X a0 z ∧ order_rel X z b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzIn).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzY HzProp).
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1}.
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z Hz).
We prove the intermediate claim HzProp: order_rel X a0 z ∧ order_rel X z b1.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzX HzProp).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
Apply (xm (a0 ∈ Y)) to the current goal.
Assume Ha0Y: a0 ∈ Y.
Apply (xm (b1 ∈ Y)) to the current goal.
Assume Hb1Y: b1 ∈ Y.
rewrite the current goal using HbYdef (from left to right).
We prove the intermediate claim HbYpow: {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} ∈ 𝒫 Y.
Apply PowerI Y {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} to the current goal.
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1}.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z Hz).
We prove the intermediate claim HbYA: {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} ∈ Ainh.
Apply (SepI (𝒫 Y) (λI : set ⇒ ∃a ∈ Y, ∃b2 ∈ Y, I = {z ∈ Y|order_rel X a z ∧ order_rel X z b2}) {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} HbYpow) to the current goal.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Y.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1Y.
Use reflexivity.
An exact proof term for the current goal is (binunionI1 Boldinh {Y} {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} (binunionI1 (Ainh ∪ Binh_ray) Cinh_ray {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} (binunionI1 Ainh Binh_ray {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1} HbYA))).
Assume Hb1notY: ¬ (b1 ∈ Y).
We prove the intermediate claim Hb1upper: ∀y : set, y ∈ Y → order_rel X y b1.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X y b1 Hso (HYsub y HyY) Hb1X (order_rel X y b1)) to the current goal.
Assume Hlt: order_rel X y b1.
An exact proof term for the current goal is Hlt.
Assume Heq: y = b1.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hb1Y': b1 ∈ Y.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Hb1notY Hb1Y').
Assume Hgt: order_rel X b1 y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxY': x ∈ Y.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HyY': y ∈ Y.
An exact proof term for the current goal is HyY.
We prove the intermediate claim HxX': x ∈ X.
An exact proof term for the current goal is (HYsub x HxY').
We prove the intermediate claim HxInSet: x ∈ {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxConj: order_rel X a0 x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) x HxInSet).
We prove the intermediate claim HxLessB1: order_rel X x b1.
An exact proof term for the current goal is (andER (order_rel X a0 x) (order_rel X x b1) HxConj).
We prove the intermediate claim Hb1InInt: b1 ∈ order_interval X x y.
An exact proof term for the current goal is (order_intervalI X x y b1 Hb1X HxLessB1 Hgt).
We prove the intermediate claim HintSub: order_interval X x y ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv x y HxY' HyY').
An exact proof term for the current goal is (Hb1notY (HintSub b1 Hb1InInt)).
We prove the intermediate claim HbYeq2: bY = {z ∈ Y|order_rel X a0 z}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim HzIn: z ∈ {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using HbYdef (from right to left).
An exact proof term for the current goal is Hz.
We prove the intermediate claim HzProp: order_rel X a0 z ∧ order_rel X z b1.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzIn).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X a0 w) z (binintersectE2 b0 Y z Hz) (andEL (order_rel X a0 z) (order_rel X z b1) HzProp)).
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z}.
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim HzProp: order_rel X a0 z.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim Hzb1: order_rel X z b1.
An exact proof term for the current goal is (Hb1upper z HzY).
rewrite the current goal using HbYdef (from left to right).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzY (andI (order_rel X a0 z) (order_rel X z b1) HzProp Hzb1)).
rewrite the current goal using HbYeq2 (from left to right).
We prove the intermediate claim HbYpow: {z ∈ Y|order_rel X a0 z} ∈ 𝒫 Y.
Apply PowerI Y {z ∈ Y|order_rel X a0 z} to the current goal.
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z}.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim HbYC: {z ∈ Y|order_rel X a0 z} ∈ Cinh_ray.
Apply (SepI (𝒫 Y) (λI : set ⇒ ∃a ∈ Y, I = {z ∈ Y|order_rel X a z}) {z ∈ Y|order_rel X a0 z} HbYpow) to the current goal.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Y.
Use reflexivity.
An exact proof term for the current goal is (binunionI1 Boldinh {Y} {z ∈ Y|order_rel X a0 z} (binunionI2 (Ainh ∪ Binh_ray) Cinh_ray {z ∈ Y|order_rel X a0 z} HbYC)).
Assume Ha0notY: ¬ (a0 ∈ Y).
Apply (xm (b1 ∈ Y)) to the current goal.
Assume Hb1Y: b1 ∈ Y.
We prove the intermediate claim Ha0lower: ∀y : set, y ∈ Y → order_rel X a0 y.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X a0 y Hso Ha0X (HYsub y HyY) (order_rel X a0 y)) to the current goal.
Assume Hlt: order_rel X a0 y.
An exact proof term for the current goal is Hlt.
Assume Heq: a0 = y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Ha0Y': a0 ∈ Y.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Ha0notY Ha0Y').
Assume Hgt: order_rel X y a0.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HyY': y ∈ Y.
An exact proof term for the current goal is HyY.
We prove the intermediate claim HxY': x ∈ Y.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HxX': x ∈ X.
An exact proof term for the current goal is (HYsub x HxY').
We prove the intermediate claim HxInSet: x ∈ {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxConj: order_rel X a0 x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) x HxInSet).
We prove the intermediate claim Ha0LessX: order_rel X a0 x.
An exact proof term for the current goal is (andEL (order_rel X a0 x) (order_rel X x b1) HxConj).
We prove the intermediate claim Ha0InInt: a0 ∈ order_interval X y x.
An exact proof term for the current goal is (order_intervalI X y x a0 Ha0X Hgt Ha0LessX).
We prove the intermediate claim HintSub: order_interval X y x ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv y x HyY' HxY').
An exact proof term for the current goal is (Ha0notY (HintSub a0 Ha0InInt)).
We prove the intermediate claim HbYeq2: bY = {z ∈ Y|order_rel X z b1}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim HzIn: z ∈ {z ∈ Y|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using HbYdef (from right to left).
An exact proof term for the current goal is Hz.
We prove the intermediate claim HzProp: order_rel X a0 z ∧ order_rel X z b1.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzIn).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X w b1) z (binintersectE2 b0 Y z Hz) (andER (order_rel X a0 z) (order_rel X z b1) HzProp)).
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X z b1}.
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim HzProp: order_rel X z b1.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim Haza: order_rel X a0 z.
An exact proof term for the current goal is (Ha0lower z HzY).
rewrite the current goal using HbYdef (from left to right).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzY (andI (order_rel X a0 z) (order_rel X z b1) Haza HzProp)).
rewrite the current goal using HbYeq2 (from left to right).
We prove the intermediate claim HbYpow: {z ∈ Y|order_rel X z b1} ∈ 𝒫 Y.
Apply PowerI Y {z ∈ Y|order_rel X z b1} to the current goal.
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X z b1}.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim HbYB: {z ∈ Y|order_rel X z b1} ∈ Binh_ray.
Apply (SepI (𝒫 Y) (λI : set ⇒ ∃b2 ∈ Y, I = {z ∈ Y|order_rel X z b2}) {z ∈ Y|order_rel X z b1} HbYpow) to the current goal.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1Y.
Use reflexivity.
An exact proof term for the current goal is (binunionI1 Boldinh {Y} {z ∈ Y|order_rel X z b1} (binunionI1 (Ainh ∪ Binh_ray) Cinh_ray {z ∈ Y|order_rel X z b1} (binunionI2 Ainh Binh_ray {z ∈ Y|order_rel X z b1} HbYB))).
Assume Hb1notY: ¬ (b1 ∈ Y).
We prove the intermediate claim Ha0lower: ∀y : set, y ∈ Y → order_rel X a0 y.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X a0 y Hso Ha0X (HYsub y HyY) (order_rel X a0 y)) to the current goal.
Assume Hlt: order_rel X a0 y.
An exact proof term for the current goal is Hlt.
Assume Heq: a0 = y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Ha0Y': a0 ∈ Y.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Ha0notY Ha0Y').
Assume Hgt: order_rel X y a0.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HyY': y ∈ Y.
An exact proof term for the current goal is HyY.
We prove the intermediate claim HxY': x ∈ Y.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HxX': x ∈ X.
An exact proof term for the current goal is (HYsub x HxY').
We prove the intermediate claim HxInSet: x ∈ {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxConj: order_rel X a0 x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) x HxInSet).
We prove the intermediate claim Ha0LessX: order_rel X a0 x.
An exact proof term for the current goal is (andEL (order_rel X a0 x) (order_rel X x b1) HxConj).
We prove the intermediate claim Ha0InInt: a0 ∈ order_interval X y x.
An exact proof term for the current goal is (order_intervalI X y x a0 Ha0X Hgt Ha0LessX).
We prove the intermediate claim HintSub: order_interval X y x ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv y x HyY' HxY').
An exact proof term for the current goal is (Ha0notY (HintSub a0 Ha0InInt)).
We prove the intermediate claim Hb1upper: ∀y : set, y ∈ Y → order_rel X y b1.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X y b1 Hso (HYsub y HyY) Hb1X (order_rel X y b1)) to the current goal.
Assume Hlt: order_rel X y b1.
An exact proof term for the current goal is Hlt.
Assume Heq: y = b1.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hb1Y': b1 ∈ Y.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Hb1notY Hb1Y').
Assume Hgt: order_rel X b1 y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxY': x ∈ Y.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HyY': y ∈ Y.
An exact proof term for the current goal is HyY.
We prove the intermediate claim HxX': x ∈ X.
An exact proof term for the current goal is (HYsub x HxY').
We prove the intermediate claim HxInSet: x ∈ {z ∈ X|order_rel X a0 z ∧ order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxConj: order_rel X a0 x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) x HxInSet).
We prove the intermediate claim HxLessB1: order_rel X x b1.
An exact proof term for the current goal is (andER (order_rel X a0 x) (order_rel X x b1) HxConj).
We prove the intermediate claim Hb1InInt: b1 ∈ order_interval X x y.
An exact proof term for the current goal is (order_intervalI X x y b1 Hb1X HxLessB1 Hgt).
We prove the intermediate claim HintSub: order_interval X x y ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv x y HxY' HyY').
An exact proof term for the current goal is (Hb1notY (HintSub b1 Hb1InInt)).
We prove the intermediate claim HbYeqY: bY = Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 b0 Y).
Let z be given.
Assume HzY: z ∈ Y.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim Haza: order_rel X a0 z.
An exact proof term for the current goal is (Ha0lower z HzY).
We prove the intermediate claim Hzb1: order_rel X z b1.
An exact proof term for the current goal is (Hb1upper z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X a0 w ∧ order_rel X w b1) z HzX (andI (order_rel X a0 z) (order_rel X z b1) Haza Hzb1)).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
rewrite the current goal using HbYeqY (from left to right).
An exact proof term for the current goal is (binunionI2 Boldinh {Y} Y (SingI Y)).
Assume Hb0B0: b0 ∈ B0.
We prove the intermediate claim HexRay: ∃b1 ∈ X, b0 = {z ∈ X|order_rel X z b1}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃b1 ∈ X, I = {z ∈ X|order_rel X z b1}) b0 Hb0B0).
Apply HexRay to the current goal.
Let b1 be given.
Assume Hb1pair.
Apply Hb1pair to the current goal.
Assume Hb1X: b1 ∈ X.
Assume Hb0eq: b0 = {z ∈ X|order_rel X z b1}.
We prove the intermediate claim HbYdef: bY = {z ∈ Y|order_rel X z b1}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 b0 Y z Hz).
We prove the intermediate claim HzIn: z ∈ {z ∈ X|order_rel X z b1}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hzb0.
We prove the intermediate claim HzProp: order_rel X z b1.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X w b1) z HzIn).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X w b1) z HzY HzProp).
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X z b1}.
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim HzProp: order_rel X z b1.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X w b1) z HzX HzProp).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
Apply (xm (b1 ∈ Y)) to the current goal.
Assume Hb1Y: b1 ∈ Y.
rewrite the current goal using HbYdef (from left to right).
We prove the intermediate claim HbYpow: {z ∈ Y|order_rel X z b1} ∈ 𝒫 Y.
Apply PowerI Y {z ∈ Y|order_rel X z b1} to the current goal.
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X z b1}.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X w b1) z Hz).
We prove the intermediate claim HbYB: {z ∈ Y|order_rel X z b1} ∈ Binh_ray.
Apply (SepI (𝒫 Y) (λI : set ⇒ ∃b2 ∈ Y, I = {z ∈ Y|order_rel X z b2}) {z ∈ Y|order_rel X z b1} HbYpow) to the current goal.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1Y.
Use reflexivity.
An exact proof term for the current goal is (binunionI1 Boldinh {Y} {z ∈ Y|order_rel X z b1} (binunionI1 (Ainh ∪ Binh_ray) Cinh_ray {z ∈ Y|order_rel X z b1} (binunionI2 Ainh Binh_ray {z ∈ Y|order_rel X z b1} HbYB))).
Assume Hb1notY: ¬ (b1 ∈ Y).
We prove the intermediate claim Hb1upper: ∀y : set, y ∈ Y → order_rel X y b1.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X y b1 Hso (HYsub y HyY) Hb1X (order_rel X y b1)) to the current goal.
Assume Hlt: order_rel X y b1.
An exact proof term for the current goal is Hlt.
Assume Heq: y = b1.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hb1Y': b1 ∈ Y.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Hb1notY Hb1Y').
Assume Hgt: order_rel X b1 y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxProp: order_rel X x b1.
We prove the intermediate claim HxInbY: x ∈ bY.
An exact proof term for the current goal is (binintersectI b0 Y x Hxb0 HxY).
We prove the intermediate claim HxInDef: x ∈ {z ∈ Y|order_rel X z b1}.
rewrite the current goal using HbYdef (from right to left).
An exact proof term for the current goal is HxInbY.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X w b1) x HxInDef).
We prove the intermediate claim Hb1InInt: b1 ∈ order_interval X x y.
An exact proof term for the current goal is (order_intervalI X x y b1 Hb1X HxProp Hgt).
We prove the intermediate claim HintSub: order_interval X x y ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv x y HxY HyY).
An exact proof term for the current goal is (Hb1notY (HintSub b1 Hb1InInt)).
We prove the intermediate claim HbYeqY: bY = Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 b0 Y).
Let z be given.
Assume HzY: z ∈ Y.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim HzProp: order_rel X z b1.
An exact proof term for the current goal is (Hb1upper z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X w b1) z HzX HzProp).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
rewrite the current goal using HbYeqY (from left to right).
An exact proof term for the current goal is (binunionI2 Boldinh {Y} Y (SingI Y)).
Assume Hb0C0: b0 ∈ C0.
We prove the intermediate claim HexRay: ∃a0 ∈ X, b0 = {z ∈ X|order_rel X a0 z}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, I = {z ∈ X|order_rel X a0 z}) b0 Hb0C0).
Apply HexRay to the current goal.
Let a0 be given.
Assume Ha0pair.
Apply Ha0pair to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb0eq: b0 = {z ∈ X|order_rel X a0 z}.
We prove the intermediate claim HbYdef: bY = {z ∈ Y|order_rel X a0 z}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 b0 Y z Hz).
We prove the intermediate claim HzIn: z ∈ {z ∈ X|order_rel X a0 z}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hzb0.
We prove the intermediate claim HzProp: order_rel X a0 z.
An exact proof term for the current goal is (SepE2 X (λw : set ⇒ order_rel X a0 w) z HzIn).
An exact proof term for the current goal is (SepI Y (λw : set ⇒ order_rel X a0 w) z HzY HzProp).
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z}.
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim HzProp: order_rel X a0 z.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X a0 w) z HzX HzProp).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
Apply (xm (a0 ∈ Y)) to the current goal.
Assume Ha0Y: a0 ∈ Y.
rewrite the current goal using HbYdef (from left to right).
We prove the intermediate claim HbYpow: {z ∈ Y|order_rel X a0 z} ∈ 𝒫 Y.
Apply PowerI Y {z ∈ Y|order_rel X a0 z} to the current goal.
Let z be given.
Assume Hz: z ∈ {z ∈ Y|order_rel X a0 z}.
An exact proof term for the current goal is (SepE1 Y (λw : set ⇒ order_rel X a0 w) z Hz).
We prove the intermediate claim HbYC: {z ∈ Y|order_rel X a0 z} ∈ Cinh_ray.
Apply (SepI (𝒫 Y) (λI : set ⇒ ∃a ∈ Y, I = {z ∈ Y|order_rel X a z}) {z ∈ Y|order_rel X a0 z} HbYpow) to the current goal.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Y.
Use reflexivity.
An exact proof term for the current goal is (binunionI1 Boldinh {Y} {z ∈ Y|order_rel X a0 z} (binunionI2 (Ainh ∪ Binh_ray) Cinh_ray {z ∈ Y|order_rel X a0 z} HbYC)).
Assume Ha0notY: ¬ (a0 ∈ Y).
We prove the intermediate claim Ha0lower: ∀y : set, y ∈ Y → order_rel X a0 y.
Let y be given.
Assume HyY: y ∈ Y.
Apply (order_rel_trichotomy_or_impred X a0 y Hso Ha0X (HYsub y HyY) (order_rel X a0 y)) to the current goal.
Assume Hlt: order_rel X a0 y.
An exact proof term for the current goal is Hlt.
Assume Heq: a0 = y.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Ha0Y': a0 ∈ Y.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (Ha0notY Ha0Y').
Assume Hgt: order_rel X y a0.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxProp: order_rel X a0 x.
We prove the intermediate claim HxInbY: x ∈ bY.
An exact proof term for the current goal is (binintersectI b0 Y x Hxb0 HxY).
We prove the intermediate claim HxInDef: x ∈ {z ∈ Y|order_rel X a0 z}.
rewrite the current goal using HbYdef (from right to left).
An exact proof term for the current goal is HxInbY.
An exact proof term for the current goal is (SepE2 Y (λw : set ⇒ order_rel X a0 w) x HxInDef).
We prove the intermediate claim Ha0InInt: a0 ∈ order_interval X y x.
An exact proof term for the current goal is (order_intervalI X y x a0 Ha0X Hgt HxProp).
We prove the intermediate claim HintSub: order_interval X y x ⊆ Y.
An exact proof term for the current goal is (convex_in_interval_property X Y Hconv y x HyY HxY).
An exact proof term for the current goal is (Ha0notY (HintSub a0 Ha0InInt)).
We prove the intermediate claim HbYeqY: bY = Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 b0 Y).
Let z be given.
Assume HzY: z ∈ Y.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim HzProp: order_rel X a0 z.
An exact proof term for the current goal is (Ha0lower z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λw : set ⇒ order_rel X a0 w) z HzX HzProp).
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
rewrite the current goal using HbYeqY (from left to right).
An exact proof term for the current goal is (binunionI2 Boldinh {Y} Y (SingI Y)).
Assume Hb0X: b0 ∈ {X}.
We prove the intermediate claim Hb0eqX: b0 = X.
An exact proof term for the current goal is (SingE X b0 Hb0X).
We prove the intermediate claim HbYeqY: bY = Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 b0 Y).
Let z be given.
Assume HzY: z ∈ Y.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HYsub z HzY).
We prove the intermediate claim Hzb0: z ∈ b0.
rewrite the current goal using Hb0eqX (from left to right).
An exact proof term for the current goal is HzX.
An exact proof term for the current goal is (binintersectI b0 Y z Hzb0 HzY).
rewrite the current goal using HbYeqY (from left to right).
An exact proof term for the current goal is (binunionI2 Boldinh {Y} Y (SingI Y)).
Apply andI to the current goal.
An exact proof term for the current goal is (binintersectI b0 Y x Hxb0 HxY).
Let z be given.
Assume Hz: z ∈ bY.
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 b0 Y z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (Hb0subV z Hzb0).
We prove the intermediate claim HzU: z ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersectI V Y z HzV HzY).
An exact proof term for the current goal is HzU.
∎