Let L and R be given.
Let α be given.
Assume Ha: ordinal α.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R α p.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
Set p0 to be the term λδ ⇒ p δ ∧ δ ≠ α of type set → prop.
Set p1 to be the term λδ ⇒ p δ ∨ δ = α of type set → prop.
Apply Hp to the current goal.
Assume Hp0: PNo_rel_strict_imv L R (ordsucc α) p0.
Assume Hp1: PNo_rel_strict_imv L R (ordsucc α) p1.
Apply Hp0 to the current goal.
Assume Hp0a: PNo_rel_strict_upperbd L (ordsucc α) p0.
Assume Hp0b: PNo_rel_strict_lowerbd R (ordsucc α) p0.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_rel_strict_upperbd L (ordsucc α) p1.
Assume Hp1b: PNo_rel_strict_lowerbd R (ordsucc α) p1.
We prove the intermediate claim Lnp0a: ¬ p0 α.
Assume H10.
Apply H10 to the current goal.
Assume H11: p α.
Assume H12: α ≠ α.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp1a: p1 α.
We will prove p α ∨ α = α.
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate claim Lap0p: PNoLt (ordsucc α) p0 α p.
Apply PNoLtI3 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ α p0 p.
Apply PNoEq_sym_ to the current goal.
Apply PNo_extend0_eq to the current goal.
We will prove ¬ p0 α.
An exact proof term for the current goal is Lnp0a.
We prove the intermediate claim Lapp1: PNoLt α p (ordsucc α) p1.
Apply PNoLtI2 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ α p p1.
Apply PNo_extend1_eq to the current goal.
We will prove p1 α.
An exact proof term for the current goal is Lp1a.
We will prove PNo_strict_upperbd L α p ∧ PNo_strict_lowerbd R α p.
Apply andI to the current goal.
Let β be given.
Assume Hb: ordinal β.
Let q be given.
Assume Hq: L β q.
We will prove PNoLt β q α p.
We prove the intermediate claim L4: PNo_downc L β q.
Apply PNo_downc_ref L β Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: β ∈ ordsucc α → PNoLt β q α p.
Assume H10: β ∈ ordsucc α.
Apply PNoLt_tra β (ordsucc α) α Hb Lsa Ha q p0 p to the current goal.
We will prove PNoLt β q (ordsucc α) p0.
Apply Hp0a β H10 q to the current goal.
We will prove PNo_downc L β q.
An exact proof term for the current goal is L4.
An exact proof term for the current goal is Lap0p.
We prove the intermediate claim L6: ∀γ ∈ ordsucc α, γ ∈ β → PNoEq_ γ p q → q γ → p0 γ.
Let γ be given.
Assume Hc1: γ ∈ ordsucc α.
Assume Hc2: γ ∈ β.
Assume H10: PNoEq_ γ p q.
Assume H11: q γ.
Apply dneg to the current goal.
Assume HNC: ¬ p0 γ.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered β Hb γ Hc2.
We prove the intermediate claim L6a: PNoLt γ q β q.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ γ q q.
Apply PNoEq_ref_ to the current goal.
We will prove q γ.
An exact proof term for the current goal is H11.
We prove the intermediate claim L6b: PNo_downc L γ q.
We will prove ∃δ, ordinal δ ∧ ∃r : set → prop, L δ r ∧ PNoLe γ q δ r.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt γ q (ordsucc α) p0.
An exact proof term for the current goal is Hp0a γ Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt (ordsucc α) p0 γ q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ γ p0 q.
Apply PNoEq_tra_ γ p0 p q to the current goal.
Apply PNoEq_sym_ to the current goal.
We will prove PNoEq_ γ p p0.
Apply ordsuccE α γ Hc1 to the current goal.
Assume H12: γ ∈ α.
Apply PNoEq_antimon_ p p0 α Ha γ H12 to the current goal.
We will prove PNoEq_ α p p0.
An exact proof term for the current goal is PNo_extend0_eq α p.
Assume H12: γ = α.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ α p p0.
An exact proof term for the current goal is PNo_extend0_eq α p.
An exact proof term for the current goal is H10.
We will prove ¬ p0 γ.
An exact proof term for the current goal is HNC.
Apply PNoLt_irref γ q to the current goal.
An exact proof term for the current goal is PNoLt_tra γ (ordsucc α) γ Lc Lsa Lc q p0 q L6c L6d.
Apply PNoLt_trichotomy_or α β p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10: PNoLt α p β q.
Apply PNoLtE α β p q H10 to the current goal.
Assume H11: PNoLt_ (α ∩ β) p q.
Apply H11 to the current goal.
Let γ be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: γ ∈ α ∩ β.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ γ p q.
Assume H13: ¬ p γ.
Assume H14: q γ.
We will prove False.
Apply binintersectE α β γ Hc to the current goal.
Assume Hc1: γ ∈ α.
Assume Hc2: γ ∈ β.
Apply L6 γ (ordsuccI1 α γ Hc1) Hc2 H12 H14 to the current goal.
Assume H15: p γ.
Assume _.
Apply H13 to the current goal.
An exact proof term for the current goal is H15.
Assume H11: α ∈ β.
Assume H12: PNoEq_ α p q.
Assume H13: q α.
We will prove False.
Apply Lnp0a to the current goal.
We will prove p0 α.
An exact proof term for the current goal is L6 α (ordsuccI2 α) H11 H12 H13.
Assume H11: β ∈ α.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H10.
Apply H10 to the current goal.
Assume H10a: α = β.
Assume H10b: PNoEq_ α p q.
Apply L5 to the current goal.
We will prove β ∈ ordsucc α.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt β q α p.
An exact proof term for the current goal is H10.
Let β be given.
Assume Hb: ordinal β.
Let q be given.
Assume Hq: R β q.
We will prove PNoLt α p β q.
We prove the intermediate claim L4: PNo_upc R β q.
Apply PNo_upc_ref R β Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: β ∈ ordsucc α → PNoLt α p β q.
Assume H10: β ∈ ordsucc α.
Apply PNoLt_tra α (ordsucc α) β Ha Lsa Hb p p1 q to the current goal.
An exact proof term for the current goal is Lapp1.
We will prove PNoLt (ordsucc α) p1 β q.
Apply Hp1b β H10 q to the current goal.
We will prove PNo_upc R β q.
An exact proof term for the current goal is L4.
We prove the intermediate claim L6: ∀γ ∈ ordsucc α, γ ∈ β → PNoEq_ γ q p → p1 γ → q γ.
Let γ be given.
Assume Hc1: γ ∈ ordsucc α.
Assume Hc2: γ ∈ β.
Assume H10: PNoEq_ γ q p.
Assume H11: p1 γ.
Apply dneg to the current goal.
Assume HNC: ¬ q γ.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered β Hb γ Hc2.
We prove the intermediate claim L6a: PNoLt β q γ q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ γ q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q γ.
An exact proof term for the current goal is HNC.
We prove the intermediate claim L6b: PNo_upc R γ q.
We will prove ∃δ, ordinal δ ∧ ∃r : set → prop, R δ r ∧ PNoLe δ r γ q.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt (ordsucc α) p1 γ q.
An exact proof term for the current goal is Hp1b γ Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt γ q (ordsucc α) p1.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ γ q p1.
Apply PNoEq_tra_ γ q p p1 to the current goal.
An exact proof term for the current goal is H10.
We will prove PNoEq_ γ p p1.
Apply ordsuccE α γ Hc1 to the current goal.
Assume H12: γ ∈ α.
Apply PNoEq_antimon_ p p1 α Ha γ H12 to the current goal.
We will prove PNoEq_ α p p1.
An exact proof term for the current goal is PNo_extend1_eq α p.
Assume H12: γ = α.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ α p p1.
An exact proof term for the current goal is PNo_extend1_eq α p.
We will prove p1 γ.
An exact proof term for the current goal is H11.
Apply PNoLt_irref γ q to the current goal.
An exact proof term for the current goal is PNoLt_tra γ (ordsucc α) γ Lc Lsa Lc q p1 q L6d L6c.
Apply PNoLt_trichotomy_or α β p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10.
An exact proof term for the current goal is H10.
Assume H10.
Apply H10 to the current goal.
Assume H10a: α = β.
Assume H10b: PNoEq_ α p q.
Apply L5 to the current goal.
We will prove β ∈ ordsucc α.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt β q α p.
Apply PNoLtE β α q p H10 to the current goal.
Assume H11: PNoLt_ (β ∩ α) q p.
Apply H11 to the current goal.
Let γ be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: γ ∈ β ∩ α.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ γ q p.
Assume H13: ¬ q γ.
Assume H14: p γ.
We will prove False.
Apply binintersectE β α γ Hc to the current goal.
Assume Hc2: γ ∈ β.
Assume Hc1: γ ∈ α.
Apply H13 to the current goal.
Apply L6 γ (ordsuccI1 α γ Hc1) Hc2 H12 to the current goal.
We will prove p1 γ.
We will prove p γ ∨ γ = α.
Apply orIL to the current goal.
An exact proof term for the current goal is H14.
Assume H11: β ∈ α.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H11: α ∈ β.
Assume H12: PNoEq_ α q p.
Assume H13: ¬ q α.
We will prove False.
Apply H13 to the current goal.
An exact proof term for the current goal is L6 α (ordsuccI2 α) H11 H12 Lp1a.
∎