Let L and R be given.
Assume HLR.
We prove the intermediate claim LLR: PNoLt_pwise (PNo_downc L) (PNo_upc R).
An exact proof term for the current goal is PNoLt_pwise_downc_upc L R HLR.
Apply ordinal_ind to the current goal.
Let α be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume IH: ∀γ ∈ α, (∃p : set → prop, PNo_rel_strict_uniq_imv L R γ p) ∨ (∃tau ∈ γ, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p).
Apply dneg to the current goal.
Assume HNC: ¬ ((∃p : set → prop, PNo_rel_strict_uniq_imv L R α p) ∨ (∃tau ∈ α, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)).
Apply not_or_and_demorgan (∃p : set → prop, PNo_rel_strict_uniq_imv L R α p) (∃tau ∈ α, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p) HNC to the current goal.
Assume HNC1: ¬ (∃p : set → prop, PNo_rel_strict_uniq_imv L R α p).
Assume HNC2: ¬ (∃tau ∈ α, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p).
We prove the intermediate claim LIH: ∀γ ∈ α, ∃p : set → prop, PNo_rel_strict_uniq_imv L R γ p.
Let γ be given.
Assume Hc: γ ∈ α.
Apply IH γ Hc to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: ∃tau ∈ γ, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p.
Apply H1 to the current goal.
Let tau be given.
Assume H2.
Apply H2 to the current goal.
Assume Ht: tau ∈ γ.
Assume H2.
Apply H2 to the current goal.
Let p be given.
Assume H3: PNo_rel_strict_split_imv L R tau p.
Apply HNC2 to the current goal.
We use tau to witness the existential quantifier.
Apply andI to the current goal.
We will prove tau ∈ α.
An exact proof term for the current goal is Ha1 γ Hc tau Ht.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R tau p.
An exact proof term for the current goal is H3.
Apply ordinal_lim_or_succ α Ha to the current goal.
Assume H1: ∀β ∈ α, ordsucc β ∈ α.
Set pl to be the term λδ ⇒ ∀p : set → prop, PNo_rel_strict_imv L R (ordsucc δ) p → p δ of type set → prop.
We prove the intermediate claim Lpl1: ∀γ, ordinal γ → γ ∈ α → PNo_rel_strict_uniq_imv L R γ pl.
Apply ordinal_ind to the current goal.
Let γ be given.
Assume Hc: ordinal γ.
Assume IH2: ∀δ ∈ γ, δ ∈ α → PNo_rel_strict_uniq_imv L R δ pl.
Assume Hc1: γ ∈ α.
Apply LIH γ Hc1 to the current goal.
Let p be given.
Assume Hp.
Apply Hp to the current goal.
Assume Hp1: PNo_rel_strict_imv L R γ p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Assume Hp2: ∀q : set → prop, PNo_rel_strict_imv L R γ q → PNoEq_ γ p q.
We prove the intermediate claim Lplpe: PNoEq_ γ pl p.
Let δ be given.
Assume Hd: δ ∈ γ.
Apply ordinal_ordsucc_In_eq γ δ Hc Hd to the current goal.
Assume Hsd: ordsucc δ ∈ γ.
We prove the intermediate claim Lsda: ordsucc δ ∈ α.
An exact proof term for the current goal is Ha1 γ Hc1 (ordsucc δ) Hsd.
Apply IH2 (ordsucc δ) Hsd Lsda to the current goal.
Assume Hpl1: PNo_rel_strict_imv L R (ordsucc δ) pl.
Assume Hpl2: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc δ) q → PNoEq_ (ordsucc δ) pl q.
We will prove pl δ ↔ p δ.
Apply Hpl2 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc δ) p.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R γ Hc p (ordsucc δ) Hsd Hp1.
We will prove δ ∈ ordsucc δ.
Apply ordsuccI2 to the current goal.
Assume Hsd: γ = ordsucc δ.
We will prove pl δ ↔ p δ.
Apply iffI to the current goal.
Assume H2: pl δ.
We will prove p δ.
Apply H2 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc δ) p.
rewrite the current goal using Hsd (from right to left).
An exact proof term for the current goal is Hp1.
Assume H2: p δ.
Let q be given.
rewrite the current goal using Hsd (from right to left).
Assume Hq: PNo_rel_strict_imv L R γ q.
We will prove q δ.
An exact proof term for the current goal is iffEL (p δ) (q δ) (Hp2 q Hq δ Hd) H2.
We will prove PNo_rel_strict_uniq_imv L R γ pl.
We will prove PNo_rel_strict_imv L R γ pl ∧ ∀q : set → prop, PNo_rel_strict_imv L R γ q → PNoEq_ γ pl q.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R γ pl.
We will prove PNo_rel_strict_upperbd L γ pl ∧ PNo_rel_strict_lowerbd R γ pl.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L γ pl.
Let β be given.
Assume Hb: β ∈ γ.
Let q be given.
Assume Hq: PNo_downc L β q.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered γ Hc β Hb.
We will prove PNoLt β q γ pl.
Apply PNoLtEq_tra β γ Lb Hc q p pl to the current goal.
We will prove PNoLt β q γ p.
An exact proof term for the current goal is Hp1a β Hb q Hq.
We will prove PNoEq_ γ p pl.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lplpe.
We will prove PNo_rel_strict_lowerbd R γ pl.
Let β be given.
Assume Hb: β ∈ γ.
Let q be given.
Assume Hq: PNo_upc R β q.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered γ Hc β Hb.
We will prove PNoLt γ pl β q.
Apply PNoEqLt_tra γ β Hc Lb pl p q to the current goal.
We will prove PNoEq_ γ pl p.
An exact proof term for the current goal is Lplpe.
We will prove PNoLt γ p β q.
An exact proof term for the current goal is Hp1b β Hb q Hq.
We will prove ∀q : set → prop, PNo_rel_strict_imv L R γ q → PNoEq_ γ pl q.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R γ q.
We will prove PNoEq_ γ pl q.
Apply PNoEq_tra_ γ pl p q to the current goal.
We will prove PNoEq_ γ pl p.
An exact proof term for the current goal is Lplpe.
We will prove PNoEq_ γ p q.
An exact proof term for the current goal is Hp2 q Hq.
We prove the intermediate claim Lpl2: ∀γ ∈ α, PNo_rel_strict_uniq_imv L R γ pl.
Let γ be given.
Assume Hc: γ ∈ α.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered α Ha γ Hc.
An exact proof term for the current goal is Lpl1 γ Lc Hc.
Apply HNC1 to the current goal.
We use pl to witness the existential quantifier.
We will prove PNo_rel_strict_uniq_imv L R α pl.
We will prove PNo_rel_strict_imv L R α pl ∧ ∀q : set → prop, PNo_rel_strict_imv L R α q → PNoEq_ α pl q.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R α pl.
We will prove PNo_rel_strict_upperbd L α pl ∧ PNo_rel_strict_lowerbd R α pl.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L α pl.
Let β be given.
Assume Hb: β ∈ α.
Let q be given.
Assume Hq: PNo_downc L β q.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc β).
An exact proof term for the current goal is ordinal_ordsucc β Lb.
We will prove PNoLt β q α pl.
Apply PNoLt_trichotomy_or β α q pl Lb Ha to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: PNoLt β q α pl.
An exact proof term for the current goal is H2.
Assume H2.
Apply H2 to the current goal.
Assume H2: β = α.
We will prove False.
Apply In_irref α to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb.
Assume H2: PNoLt α pl β q.
Apply PNoLtE α β pl q H2 to the current goal.
Assume H3: PNoLt_ (α ∩ β) pl q.
Apply H3 to the current goal.
Let γ be given.
Assume H4.
Apply H4 to the current goal.
Assume Hc: γ ∈ α ∩ β.
Apply binintersectE α β γ Hc to the current goal.
Assume Hc1 Hc2.
Assume H5.
Apply H5 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoEq_ γ pl q.
Assume H6: ¬ pl γ.
Assume H7: q γ.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered β Lb γ Hc2.
We prove the intermediate claim Lsc: ordinal (ordsucc γ).
An exact proof term for the current goal is ordinal_ordsucc γ Lc.
We will prove False.
Apply H6 to the current goal.
We will prove pl γ.
Let p be given.
Assume Hp: PNo_rel_strict_imv L R (ordsucc γ) p.
We will prove p γ.
Apply Hp to the current goal.
Assume Hp1 Hp2.
We prove the intermediate claim Lqp: PNoLt γ q (ordsucc γ) p.
Apply Hp1 γ (ordsuccI2 γ) q to the current goal.
We will prove PNo_downc L γ q.
Apply PNoLe_downc L β γ q q Lb Lc to the current goal.
We will prove PNo_downc L β q.
An exact proof term for the current goal is Hq.
We will prove PNoLe γ q β q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt γ q β q.
Apply PNoLtI2 to the current goal.
We will prove γ ∈ β.
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 H7.
Apply PNoLtE γ (ordsucc γ) q p Lqp to the current goal.
Assume H6: PNoLt_ (γ ∩ ordsucc γ) q p.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: δ ∈ γ ∩ ordsucc γ.
Apply binintersectE γ (ordsucc γ) δ Hd to the current goal.
Assume Hd1 Hd2.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ δ q p.
Assume H8: ¬ q δ.
Assume H9: p δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered γ Lc δ Hd1.
We prove the intermediate claim Lda: δ ∈ α.
An exact proof term for the current goal is Ha1 γ Hc1 δ Hd1.
We prove the intermediate claim Lsda: ordsucc δ ∈ α.
An exact proof term for the current goal is H1 δ Lda.
We prove the intermediate claim Lpld: pl δ.
Apply Lpl2 (ordsucc δ) Lsda to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc δ) q → PNoEq_ (ordsucc δ) pl q.
We prove the intermediate claim Lpld1: PNoEq_ (ordsucc δ) pl p.
Apply Hpl3 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc δ) p.
Apply PNo_rel_strict_imv_antimon L R (ordsucc γ) Lsc p to the current goal.
We will prove ordsucc δ ∈ ordsucc γ.
Apply ordinal_ordsucc_In to the current goal.
An exact proof term for the current goal is Lc.
We will prove δ ∈ γ.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hp.
An exact proof term for the current goal is iffER (pl δ) (p δ) (Lpld1 δ (ordsuccI2 δ)) H9.
We prove the intermediate claim Lnpld: ¬ pl δ.
Assume H10: pl δ.
Apply H8 to the current goal.
An exact proof term for the current goal is iffEL (pl δ) (q δ) (H5 δ Hd1) H10.
We will prove False.
An exact proof term for the current goal is Lnpld Lpld.
Assume H6: γ ∈ ordsucc γ.
Assume H7: PNoEq_ γ q p.
Assume H8: p γ.
An exact proof term for the current goal is H8.
Assume H6: ordsucc γ ∈ γ.
We will prove False.
An exact proof term for the current goal is In_no2cycle γ (ordsucc γ) (ordsuccI2 γ) H6.
Assume H3: α ∈ β.
We will prove False.
An exact proof term for the current goal is In_no2cycle β α Hb H3.
Assume H3: β ∈ α.
Assume H4: PNoEq_ β pl q.
Assume H5: ¬ pl β.
We will prove False.
Apply H5 to the current goal.
We will prove pl β.
Let p be given.
Assume Hp: PNo_rel_strict_imv L R (ordsucc β) p.
We will prove p β.
Apply Hp to the current goal.
Assume Hp1 Hp2.
We prove the intermediate claim Lqp: PNoLt β q (ordsucc β) p.
An exact proof term for the current goal is Hp1 β (ordsuccI2 β) q Hq.
Apply PNoLtE β (ordsucc β) q p Lqp to the current goal.
Assume H6: PNoLt_ (β ∩ ordsucc β) q p.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: δ ∈ β ∩ ordsucc β.
Apply binintersectE β (ordsucc β) δ Hd to the current goal.
Assume Hd1 Hd2.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ δ q p.
Assume H8: ¬ q δ.
Assume H9: p δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Lb δ Hd1.
We prove the intermediate claim Lda: δ ∈ α.
An exact proof term for the current goal is Ha1 β Hb δ Hd1.
We prove the intermediate claim Lsda: ordsucc δ ∈ α.
An exact proof term for the current goal is H1 δ Lda.
We prove the intermediate claim Lpld: pl δ.
Apply Lpl2 (ordsucc δ) Lsda to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc δ) q → PNoEq_ (ordsucc δ) pl q.
We prove the intermediate claim Lpld1: PNoEq_ (ordsucc δ) pl p.
Apply Hpl3 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc δ) p.
Apply PNo_rel_strict_imv_antimon L R (ordsucc β) Lsb p to the current goal.
We will prove ordsucc δ ∈ ordsucc β.
Apply ordinal_ordsucc_In to the current goal.
An exact proof term for the current goal is Lb.
We will prove δ ∈ β.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hp.
An exact proof term for the current goal is iffER (pl δ) (p δ) (Lpld1 δ (ordsuccI2 δ)) H9.
We prove the intermediate claim Lnpld: ¬ pl δ.
Assume H10: pl δ.
Apply H8 to the current goal.
An exact proof term for the current goal is iffEL (pl δ) (q δ) (H4 δ Hd1) H10.
We will prove False.
An exact proof term for the current goal is Lnpld Lpld.
Assume H6: β ∈ ordsucc β.
Assume H7: PNoEq_ β q p.
Assume H8: p β.
An exact proof term for the current goal is H8.
Assume H6: ordsucc β ∈ β.
We will prove False.
An exact proof term for the current goal is In_no2cycle β (ordsucc β) (ordsuccI2 β) H6.
We will prove PNo_rel_strict_lowerbd R α pl.
Let β be given.
Assume Hb: β ∈ α.
Let q be given.
Assume Hq: PNo_upc R β q.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc β).
An exact proof term for the current goal is ordinal_ordsucc β Lb.
We prove the intermediate claim Lsba: ordsucc β ∈ α.
An exact proof term for the current goal is H1 β Hb.
We will prove PNoLt α pl β q.
Apply PNoLt_trichotomy_or α β pl q Ha Lb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: PNoLt α pl β q.
An exact proof term for the current goal is H2.
Assume H2.
Apply H2 to the current goal.
Assume H2: α = β.
We will prove False.
Apply In_irref α to the current goal.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hb.
Assume H2: PNoLt β q α pl.
Apply PNoLtE β α q pl H2 to the current goal.
Assume H3: PNoLt_ (β ∩ α) q pl.
Apply H3 to the current goal.
Let γ be given.
Assume H4.
Apply H4 to the current goal.
Assume Hc: γ ∈ β ∩ α.
Apply binintersectE β α γ Hc to the current goal.
Assume Hc2 Hc1.
Assume H5.
Apply H5 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoEq_ γ q pl.
Assume H6: ¬ q γ.
Assume H7: pl γ.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered β Lb γ Hc2.
We prove the intermediate claim Lsc: ordinal (ordsucc γ).
An exact proof term for the current goal is ordinal_ordsucc γ Lc.
We prove the intermediate claim Lsca: ordsucc γ ∈ α.
An exact proof term for the current goal is H1 γ Hc1.
We will prove False.
Apply Lpl2 (ordsucc γ) Lsca to the current goal.
Assume Hpl2: PNo_rel_strict_imv L R (ordsucc γ) pl.
Assume _.
Apply Hpl2 to the current goal.
Assume _.
Assume Hpl2b: PNo_rel_strict_lowerbd R (ordsucc γ) pl.
We prove the intermediate claim Lplq: PNoLt (ordsucc γ) pl γ q.
Apply Hpl2b γ (ordsuccI2 γ) q to the current goal.
We will prove PNo_upc R γ q.
Apply PNoLe_upc R β γ q q Lb Lc to the current goal.
We will prove PNo_upc R β q.
An exact proof term for the current goal is Hq.
We will prove PNoLe β q γ q.
Apply PNoLeI1 β γ q q to the current goal.
We will prove PNoLt β q γ q.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ β.
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 H6.
We prove the intermediate claim Lqpl: PNoLt γ q (ordsucc γ) pl.
Apply PNoLtI2 to the current goal.
We will prove γ ∈ ordsucc γ.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ γ q pl.
An exact proof term for the current goal is H5.
We will prove pl γ.
An exact proof term for the current goal is H7.
We will prove False.
Apply PNoLt_irref γ q to the current goal.
An exact proof term for the current goal is PNoLt_tra γ (ordsucc γ) γ Lc Lsc Lc q pl q Lqpl Lplq.
Assume H3: β ∈ α.
Assume H4: PNoEq_ β q pl.
Assume H5: pl β.
Apply Lpl2 (ordsucc β) Lsba to the current goal.
Assume Hpl2: PNo_rel_strict_imv L R (ordsucc β) pl.
Assume _.
Apply Hpl2 to the current goal.
Assume _.
Assume Hpl2b: PNo_rel_strict_lowerbd R (ordsucc β) pl.
We prove the intermediate claim Lplq: PNoLt (ordsucc β) pl β q.
Apply Hpl2b β (ordsuccI2 β) q to the current goal.
We will prove PNo_upc R β q.
An exact proof term for the current goal is Hq.
We prove the intermediate claim Lqpl: PNoLt β q (ordsucc β) pl.
Apply PNoLtI2 to the current goal.
We will prove β ∈ ordsucc β.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ β q pl.
An exact proof term for the current goal is H4.
We will prove pl β.
An exact proof term for the current goal is H5.
We will prove False.
Apply PNoLt_irref β q to the current goal.
An exact proof term for the current goal is PNoLt_tra β (ordsucc β) β Lb Lsb Lb q pl q Lqpl Lplq.
Assume H3: α ∈ β.
We will prove False.
An exact proof term for the current goal is In_no2cycle β α Hb H3.
We will prove ∀q : set → prop, PNo_rel_strict_imv L R α q → PNoEq_ α pl q.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R α q.
Let γ be given.
Assume Hc: γ ∈ α.
We will prove pl γ ↔ q γ.
We prove the intermediate claim Lsca: ordsucc γ ∈ α.
An exact proof term for the current goal is H1 γ Hc.
Apply Lpl2 (ordsucc γ) Lsca to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc γ) q → PNoEq_ (ordsucc γ) pl q.
Apply Hpl3 to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc γ) q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R α Ha q (ordsucc γ) Lsca Hq.
We will prove γ ∈ ordsucc γ.
Apply ordsuccI2 to the current goal.
Assume H1: ∃β ∈ α, α = ordsucc β.
Apply H1 to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ α.
Assume Hab: α = ordsucc β.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc β).
rewrite the current goal using Hab (from right to left).
An exact proof term for the current goal is Ha.
We prove the intermediate claim Lbsb1: β ∩ ordsucc β = β.
Apply binintersect_Subq_eq_1 to the current goal.
Apply ordsuccI1 to the current goal.
We prove the intermediate claim Lbsb2: ordsucc β ∩ β = β.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is Lbsb1.
Apply LIH β Hb to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_uniq_imv L R β p.
Apply Hp to the current goal.
Assume Hp0: PNo_rel_strict_imv L R β p.
Apply Hp0 to the current goal.
Assume Hp1: ∀γ ∈ β, ∀q : set → prop, PNo_downc L γ q → PNoLt γ q β p.
Assume Hp2: ∀γ ∈ β, ∀q : set → prop, PNo_upc R γ q → PNoLt β p γ q.
Assume Hp3: ∀q : set → prop, PNo_rel_strict_imv L R β q → PNoEq_ β p q.
Set p0 to be the term λδ ⇒ p δ ∧ δ ≠ β of type set → prop.
Set p1 to be the term λδ ⇒ p δ ∨ δ = β of type set → prop.
We prove the intermediate claim Lp0e: PNoEq_ β p0 p.
Let γ be given.
Assume Hc: γ ∈ β.
We will prove p0 γ ↔ p γ.
Apply iffI to the current goal.
Assume H2: p γ ∧ γ ≠ β.
We will prove p γ.
Apply H2 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
Assume H2: p γ.
We will prove p γ ∧ γ ≠ β.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
Assume H3: γ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lp0b: ¬ p0 β.
Assume H2: p β ∧ β ≠ β.
Apply H2 to the current goal.
Assume _ H2.
Apply H2 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp0p: PNoLt (ordsucc β) p0 β p.
Apply PNoLtI3 to the current goal.
We will prove β ∈ ordsucc β.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ β p0 p.
An exact proof term for the current goal is Lp0e.
We will prove ¬ p0 β.
An exact proof term for the current goal is Lp0b.
We prove the intermediate claim Lp1e: PNoEq_ β p p1.
Let γ be given.
Assume Hc: γ ∈ β.
We will prove p γ ↔ p1 γ.
Apply iffI to the current goal.
Assume H2: p γ.
We will prove p γ ∨ γ = β.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Assume H2: p γ ∨ γ = β.
We will prove p γ.
Apply H2 to the current goal.
Assume H3: p γ.
An exact proof term for the current goal is H3.
Assume H3: γ = β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lp1b: p1 β.
We will prove p β ∨ β = β.
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate claim Lpp1: PNoLt β p (ordsucc β) p1.
Apply PNoLtI2 to the current goal.
We will prove β ∈ ordsucc β.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ β p p1.
An exact proof term for the current goal is Lp1e.
We will prove p1 β.
An exact proof term for the current goal is Lp1b.
We prove the intermediate claim Lnotboth: ¬ (PNo_rel_strict_imv L R α p0 ∧ PNo_rel_strict_imv L R α p1).
rewrite the current goal using Hab (from left to right).
Assume H2.
Apply HNC2 to the current goal.
We use β to witness the existential quantifier.
Apply andI to the current goal.
We will prove β ∈ α.
An exact proof term for the current goal is Hb.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R β p.
An exact proof term for the current goal is H2.
We prove the intermediate claim Lcases: (∀q : set → prop, PNo_downc L β q → ¬ PNoEq_ β p q) ∨ (∀q : set → prop, PNo_upc R β q → ¬ PNoEq_ β p q).
rewrite the current goal using eq_or_nand (from left to right).
Assume H2.
Apply H2 to the current goal.
Assume H2: ¬ (∀q : set → prop, PNo_downc L β q → ¬ PNoEq_ β p q).
Assume H3: ¬ (∀q : set → prop, PNo_upc R β q → ¬ PNoEq_ β p q).
Apply H2 to the current goal.
Let q0 be given.
Assume H4: PNo_downc L β q0.
Assume H5: PNoEq_ β p q0.
Apply H3 to the current goal.
Let q1 be given.
Assume H6: PNo_upc R β q1.
Assume H7: PNoEq_ β p q1.
We prove the intermediate claim L2: PNoLt β q0 β q1.
An exact proof term for the current goal is LLR β Lb q0 H4 β Lb q1 H6.
Apply PNoLt_irref β q0 to the current goal.
Apply PNoLtLe_tra β β β Lb Lb Lb q0 q1 q0 L2 to the current goal.
We will prove PNoLe β q1 β q0.
We will prove PNoLt β q1 β q0 ∨ β = β ∧ PNoEq_ β q1 q0.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
We will prove PNoEq_ β q1 q0.
Apply PNoEq_tra_ β q1 p q0 to the current goal.
We will prove PNoEq_ β q1 p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H7.
We will prove PNoEq_ β p q0.
An exact proof term for the current goal is H5.
We will prove False.
Apply Lcases to the current goal.
Assume H2: ∀q : set → prop, PNo_downc L β q → ¬ PNoEq_ β p q.
We prove the intermediate claim Lp0imv: PNo_rel_strict_imv L R (ordsucc β) p0.
We will prove PNo_rel_strict_upperbd L (ordsucc β) p0 ∧ PNo_rel_strict_lowerbd R (ordsucc β) p0.
Apply andI to the current goal.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Let q be given.
Assume H3: PNo_downc L γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc β) Lsb γ Hc.
We will prove PNoLt γ q (ordsucc β) p0.
Apply ordsuccE β γ Hc to the current goal.
Assume H4: γ ∈ β.
We prove the intermediate claim L1: PNoLt γ q β p.
An exact proof term for the current goal is Hp1 γ H4 q H3.
Apply PNoLtE γ β q p L1 to the current goal.
Assume H5: PNoLt_ (γ ∩ β) q p.
Apply H5 to the current goal.
Let δ be given.
Assume H6.
Apply H6 to the current goal.
Assume Hd: δ ∈ γ ∩ β.
Assume H6.
Apply H6 to the current goal.
Assume H6.
Apply H6 to the current goal.
Assume H6: PNoEq_ δ q p.
Assume H7: ¬ q δ.
Assume H8: p δ.
Apply binintersectE γ β δ Hd to the current goal.
Assume Hd1: δ ∈ γ.
Assume Hd2: δ ∈ β.
We will prove PNoLt γ q (ordsucc β) p0.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (γ ∩ ordsucc β) q p0.
We will prove ∃β ∈ γ ∩ ordsucc β, PNoEq_ β q p0 ∧ ¬ q β ∧ p0 β.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ γ ∩ ordsucc β.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hd2.
Apply and3I to the current goal.
We will prove PNoEq_ δ q p0.
Apply PNoEq_tra_ δ q p p0 to the current goal.
An exact proof term for the current goal is H6.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p β Lb δ Hd2 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove ¬ q δ.
An exact proof term for the current goal is H7.
We will prove p0 δ.
We will prove p δ ∧ δ ≠ β.
Apply andI to the current goal.
An exact proof term for the current goal is H8.
Assume H9: δ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is Hd2.
Assume H5: γ ∈ β.
Assume H6: PNoEq_ γ q p.
Assume H7: p γ.
We will prove PNoLt γ q (ordsucc β) p0.
Apply PNoLtI2 to the current goal.
We will prove γ ∈ ordsucc β.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H5.
We will prove PNoEq_ γ q p0.
Apply PNoEq_tra_ γ q p p0 to the current goal.
We will prove PNoEq_ γ q p.
An exact proof term for the current goal is H6.
We will prove PNoEq_ γ p p0.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p β Lb γ H5 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove p0 γ.
We will prove p γ ∧ γ ≠ β.
Apply andI to the current goal.
An exact proof term for the current goal is H7.
Assume H8: γ = β.
Apply In_irref γ to the current goal.
rewrite the current goal using H8 (from left to right) at position 2.
An exact proof term for the current goal is H5.
Assume H5: β ∈ γ.
We will prove False.
An exact proof term for the current goal is In_no2cycle γ β H4 H5.
Assume H4: γ = β.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt β q (ordsucc β) p0.
Apply PNoLt_trichotomy_or β (ordsucc β) q p0 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5.
An exact proof term for the current goal is H5.
Assume H5.
Apply H5 to the current goal.
Assume H5: β = ordsucc β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc β) p0 β q.
Apply PNoLtE (ordsucc β) β p0 q H5 to the current goal.
rewrite the current goal using Lbsb2 (from left to right).
Assume H6: PNoLt_ β p0 q.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: δ ∈ β.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ δ p0 q.
Assume H8: ¬ p0 δ.
Assume H9: q δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Lb δ Hd.
We prove the intermediate claim L2: PNoLt β p δ q.
Apply PNoLtI3 to the current goal.
We will prove δ ∈ β.
An exact proof term for the current goal is Hd.
We will prove PNoEq_ δ p q.
Apply PNoEq_tra_ δ p p0 q to the current goal.
We will prove PNoEq_ δ p p0.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p β Lb δ Hd to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove PNoEq_ δ p0 q.
An exact proof term for the current goal is H7.
We will prove ¬ p δ.
Assume H10: p δ.
Apply H8 to the current goal.
We will prove p δ ∧ δ ≠ β.
Apply andI to the current goal.
An exact proof term for the current goal is H10.
Assume H11: δ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H11 (from right to left) at position 1.
An exact proof term for the current goal is Hd.
We prove the intermediate claim L3: PNoLt δ q β p.
Apply Hp1 δ Hd q to the current goal.
We will prove PNo_downc L δ q.
Apply PNoLe_downc L γ δ q q Lc Ld H3 to the current goal.
We will prove PNoLe δ q γ q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt δ q γ q.
Apply PNoLtI2 to the current goal.
We will prove δ ∈ γ.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd.
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 H9.
Apply PNoLt_irref δ q to the current goal.
We will prove PNoLt δ q δ q.
An exact proof term for the current goal is PNoLt_tra δ β δ Ld Lb Ld q p q L3 L2.
Assume H6: ordsucc β ∈ β.
We will prove False.
Apply In_no2cycle (ordsucc β) β H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H6: β ∈ ordsucc β.
Assume H7: PNoEq_ β p0 q.
We will prove False.
Apply H2 q to the current goal.
We will prove PNo_downc L β q.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3.
We will prove PNoEq_ β p q.
Apply PNoEq_tra_ β p p0 q to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp0e.
An exact proof term for the current goal is H7.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Let q be given.
Assume H3: PNo_upc R γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc β) Lsb γ Hc.
We will prove PNoLt (ordsucc β) p0 γ q.
Apply ordsuccE β γ Hc to the current goal.
Assume H4: γ ∈ β.
Apply PNoLt_tra (ordsucc β) β γ Lsb Lb Lc p0 p q Lp0p to the current goal.
We will prove PNoLt β p γ q.
Apply Hp2 γ H4 q to the current goal.
We will prove PNo_upc R γ q.
An exact proof term for the current goal is H3.
Assume H4: γ = β.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt (ordsucc β) p0 β q.
Apply PNoLt_trichotomy_or β (ordsucc β) q p0 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt β q (ordsucc β) p0.
Apply PNoLtE β (ordsucc β) q p0 H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Assume H6: PNoLt_ β q p0.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume H8: δ ∈ β.
Assume H9.
Apply H9 to the current goal.
Assume H9.
Apply H9 to the current goal.
Assume H9: PNoEq_ δ q p0.
Assume H10: ¬ q δ.
Assume H11: p0 δ.
We will prove False.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Lb δ H8.
We prove the intermediate claim L4: PNoLt β p δ q.
Apply Hp2 δ H8 q to the current goal.
We will prove PNo_upc R δ q.
Apply PNoLe_upc R γ δ q q Lc Ld H3 to the current goal.
We will prove PNoLe γ q δ q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt γ q δ q.
Apply PNoLtI3 to the current goal.
We will prove δ ∈ γ.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8.
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 H10.
We prove the intermediate claim L5: PNoLt δ q β p.
Apply PNoLtI2 to the current goal.
We will prove δ ∈ β.
An exact proof term for the current goal is H8.
We will prove PNoEq_ δ q p.
Apply PNoEq_tra_ δ q p0 p to the current goal.
An exact proof term for the current goal is H9.
We will prove PNoEq_ δ p0 p.
Apply PNoEq_antimon_ p0 p β Lb δ H8 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove p δ.
Apply H11 to the current goal.
Assume H12 _.
An exact proof term for the current goal is H12.
Apply PNoLt_irref β p to the current goal.
An exact proof term for the current goal is PNoLt_tra β δ β Lb Ld Lb p q p L4 L5.
Assume H6: β ∈ ordsucc β.
Assume H7: PNoEq_ β q p0.
Assume H8: p β ∧ β ≠ β.
We will prove False.
Apply H8 to the current goal.
Assume _ H9.
Apply H9 to the current goal.
Use reflexivity.
Assume H6: ordsucc β ∈ β.
We will prove False.
Apply In_no2cycle (ordsucc β) β H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: β = ordsucc β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc β) p0 β q.
An exact proof term for the current goal is H5.
Apply HNC1 to the current goal.
We use p0 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
We will prove PNo_rel_strict_uniq_imv L R (ordsucc β) p0.
We will prove PNo_rel_strict_imv L R (ordsucc β) p0 ∧ ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc β) q → PNoEq_ (ordsucc β) p0 q.
Apply andI to the current goal.
An exact proof term for the current goal is Lp0imv.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R (ordsucc β) q.
We will prove PNoEq_ (ordsucc β) p0 q.
We prove the intermediate claim Lqb: PNo_rel_strict_imv L R β q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R (ordsucc β) Lsb q β (ordsuccI2 β) Hq.
We prove the intermediate claim Lpqe: PNoEq_ β p q.
An exact proof term for the current goal is Hp3 q Lqb.
Apply xm (q β) to the current goal.
Assume Hq1: q β.
We will prove False.
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc β) p0.
An exact proof term for the current goal is Lp0imv.
We will prove PNo_rel_strict_imv L R (ordsucc β) p1.
Apply PNoEq_rel_strict_imv L R (ordsucc β) Lsb q p1 to the current goal.
We will prove PNoEq_ (ordsucc β) q p1.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Apply ordsuccE β γ Hc to the current goal.
Assume H3: γ ∈ β.
We prove the intermediate claim Lpqce: p γ ↔ q γ.
An exact proof term for the current goal is Lpqe γ H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove q γ ↔ p1 γ.
Apply iffI to the current goal.
Assume H4: q γ.
We will prove p γ ∨ γ = β.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqpc H4.
Assume H4: p γ ∨ γ = β.
Apply H4 to the current goal.
An exact proof term for the current goal is Hpqc.
Assume H5: γ = β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H3: γ = β.
We will prove q γ ↔ p1 γ.
Apply iffI to the current goal.
Assume _.
We will prove p γ ∨ γ = β.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Assume _.
We will prove q γ.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hq1.
We will prove PNo_rel_strict_imv L R (ordsucc β) q.
An exact proof term for the current goal is Hq.
Assume Hq0: ¬ q β.
We will prove PNoEq_ (ordsucc β) p0 q.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Apply ordsuccE β γ Hc to the current goal.
Assume H3: γ ∈ β.
We prove the intermediate claim Lpqce: p γ ↔ q γ.
An exact proof term for the current goal is Lpqe γ H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove p0 γ ↔ q γ.
Apply iffI to the current goal.
Assume H4: p γ ∧ γ ≠ β.
Apply H4 to the current goal.
Assume H5: p γ.
Assume _.
An exact proof term for the current goal is Hpqc H5.
Assume H4: q γ.
We will prove p γ ∧ γ ≠ β.
Apply andI to the current goal.
We will prove p γ.
An exact proof term for the current goal is Hqpc H4.
We will prove γ ≠ β.
Assume H5: γ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H3: γ = β.
We will prove p0 γ ↔ q γ.
Apply iffI to the current goal.
Assume H4: p γ ∧ γ ≠ β.
Apply H4 to the current goal.
Assume _ H5.
We will prove False.
An exact proof term for the current goal is H5 H3.
Assume H4: q γ.
We will prove False.
Apply Hq0 to the current goal.
We will prove q β.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4.
Assume H2: ∀q : set → prop, PNo_upc R β q → ¬ PNoEq_ β p q.
We prove the intermediate claim Lp1imv: PNo_rel_strict_imv L R (ordsucc β) p1.
We will prove PNo_rel_strict_upperbd L (ordsucc β) p1 ∧ PNo_rel_strict_lowerbd R (ordsucc β) p1.
Apply andI to the current goal.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Let q be given.
Assume H3: PNo_downc L γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc β) Lsb γ Hc.
We will prove PNoLt γ q (ordsucc β) p1.
Apply ordsuccE β γ Hc to the current goal.
Assume H4: γ ∈ β.
Apply PNoLt_tra γ β (ordsucc β) Lc Lb Lsb q p p1 to the current goal.
We will prove PNoLt γ q β p.
Apply Hp1 γ H4 q to the current goal.
We will prove PNo_downc L γ q.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Lpp1.
Assume H4: γ = β.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt β q (ordsucc β) p1.
Apply PNoLt_trichotomy_or β (ordsucc β) q p1 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt β q (ordsucc β) p1.
An exact proof term for the current goal is H5.
Assume H5.
Apply H5 to the current goal.
Assume H5: β = ordsucc β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc β) p1 β q.
Apply PNoLtE (ordsucc β) β p1 q H5 to the current goal.
rewrite the current goal using Lbsb2 (from left to right).
Assume H6: PNoLt_ β p1 q.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume H8: δ ∈ β.
Assume H9.
Apply H9 to the current goal.
Assume H9.
Apply H9 to the current goal.
Assume H9: PNoEq_ δ p1 q.
Assume H10: ¬ p1 δ.
Assume H11: q δ.
We will prove False.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Lb δ H8.
We prove the intermediate claim L4: PNoLt δ q β p.
Apply Hp1 δ H8 q to the current goal.
We will prove PNo_downc L δ q.
Apply PNoLe_downc L γ δ q q Lc Ld H3 to the current goal.
We will prove PNoLe δ q γ q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt δ q γ q.
Apply PNoLtI2 to the current goal.
We will prove δ ∈ γ.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8.
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 L5: PNoLt β p δ q.
Apply PNoLtI3 to the current goal.
We will prove δ ∈ β.
An exact proof term for the current goal is H8.
We will prove PNoEq_ δ p q.
Apply PNoEq_tra_ δ p p1 q to the current goal.
We will prove PNoEq_ δ p p1.
Apply PNoEq_antimon_ p p1 β Lb δ H8 to the current goal.
An exact proof term for the current goal is Lp1e.
An exact proof term for the current goal is H9.
We will prove ¬ p δ.
Assume H12: p δ.
Apply H10 to the current goal.
We will prove p δ ∨ δ = β.
Apply orIL to the current goal.
An exact proof term for the current goal is H12.
Apply PNoLt_irref β p to the current goal.
An exact proof term for the current goal is PNoLt_tra β δ β Lb Ld Lb p q p L5 L4.
Assume H6: ordsucc β ∈ β.
We will prove False.
Apply In_no2cycle (ordsucc β) β H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H6: β ∈ ordsucc β.
Assume H7: PNoEq_ β p1 q.
Assume H8: ¬ p1 β.
We will prove False.
Apply H8 to the current goal.
We will prove p β ∨ β = β.
Apply orIR to the current goal.
Use reflexivity.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Let q be given.
Assume H3: PNo_upc R γ q.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered (ordsucc β) Lsb γ Hc.
We will prove PNoLt (ordsucc β) p1 γ q.
Apply ordsuccE β γ Hc to the current goal.
Assume H4: γ ∈ β.
We prove the intermediate claim L1: PNoLt β p γ q.
An exact proof term for the current goal is Hp2 γ H4 q H3.
Apply PNoLtE β γ p q L1 to the current goal.
Assume H5: PNoLt_ (β ∩ γ) p q.
Apply H5 to the current goal.
Let δ be given.
Assume H6.
Apply H6 to the current goal.
Assume Hd: δ ∈ β ∩ γ.
Assume H6.
Apply H6 to the current goal.
Assume H6.
Apply H6 to the current goal.
Assume H6: PNoEq_ δ p q.
Assume H7: ¬ p δ.
Assume H8: q δ.
Apply binintersectE β γ δ Hd to the current goal.
Assume Hd2: δ ∈ β.
Assume Hd1: δ ∈ γ.
We will prove PNoLt (ordsucc β) p1 γ q.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (ordsucc β ∩ γ) p1 q.
We will prove ∃β ∈ ordsucc β ∩ γ, PNoEq_ β p1 q ∧ ¬ p1 β ∧ q β.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ ordsucc β ∩ γ.
Apply binintersectI to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hd2.
An exact proof term for the current goal is Hd1.
Apply and3I to the current goal.
We will prove PNoEq_ δ p1 q.
Apply PNoEq_tra_ δ p1 p q to the current goal.
Apply PNoEq_antimon_ p1 p β Lb δ Hd2 to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
An exact proof term for the current goal is H6.
We will prove ¬ p1 δ.
Assume H9: p δ ∨ δ = β.
We will prove False.
Apply H9 to the current goal.
An exact proof term for the current goal is H7.
Assume H10: δ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd2.
We will prove q δ.
An exact proof term for the current goal is H8.
Assume H5: β ∈ γ.
We will prove False.
An exact proof term for the current goal is In_no2cycle γ β H4 H5.
Assume H5: γ ∈ β.
Assume H6: PNoEq_ γ p q.
Assume H7: ¬ p γ.
We will prove PNoLt (ordsucc β) p1 γ q.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ ordsucc β.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H5.
We will prove PNoEq_ γ p1 q.
Apply PNoEq_tra_ γ p1 p q to the current goal.
We will prove PNoEq_ γ p1 p.
Apply PNoEq_antimon_ p1 p β Lb γ H5 to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
We will prove PNoEq_ γ p q.
An exact proof term for the current goal is H6.
We will prove ¬ p1 γ.
Assume H8: p γ ∨ γ = β.
Apply H8 to the current goal.
An exact proof term for the current goal is H7.
Assume H9: γ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is H5.
Assume H4: γ = β.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt (ordsucc β) p1 β q.
Apply PNoLt_trichotomy_or β (ordsucc β) q p1 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt β q (ordsucc β) p1.
Apply PNoLtE β (ordsucc β) q p1 H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Assume H6: PNoLt_ β q p1.
Apply H6 to the current goal.
Let δ be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: δ ∈ β.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ δ q p1.
Assume H8: ¬ q δ.
Assume H9: p1 δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Lb δ Hd.
We prove the intermediate claim L2: PNoLt δ q β p.
Apply PNoLtI2 to the current goal.
We will prove δ ∈ β.
An exact proof term for the current goal is Hd.
We will prove PNoEq_ δ q p.
Apply PNoEq_tra_ δ q p1 p to the current goal.
We will prove PNoEq_ δ q p1.
An exact proof term for the current goal is H7.
We will prove PNoEq_ δ p1 p.
Apply PNoEq_antimon_ p1 p β Lb δ Hd to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
We will prove p δ.
Apply H9 to the current goal.
Assume H10: p δ.
An exact proof term for the current goal is H10.
Assume H10: δ = β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd.
We prove the intermediate claim L3: PNoLt β p δ q.
Apply Hp2 δ Hd q to the current goal.
We will prove PNo_upc R δ q.
Apply PNoLe_upc R γ δ q q Lc Ld H3 to the current goal.
We will prove PNoLe γ q δ q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt γ q δ q.
Apply PNoLtI3 to the current goal.
We will prove δ ∈ γ.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd.
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 H8.
Apply PNoLt_irref δ q to the current goal.
We will prove PNoLt δ q δ q.
An exact proof term for the current goal is PNoLt_tra δ β δ Ld Lb Ld q p q L2 L3.
Assume H6: β ∈ ordsucc β.
Assume H7: PNoEq_ β q p1.
We will prove False.
Apply H2 q to the current goal.
We will prove PNo_upc R β q.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3.
We will prove PNoEq_ β p q.
Apply PNoEq_tra_ β p p1 q to the current goal.
An exact proof term for the current goal is Lp1e.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H7.
Assume H6: ordsucc β ∈ β.
We will prove False.
Apply In_no2cycle (ordsucc β) β H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: β = ordsucc β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5.
An exact proof term for the current goal is H5.
Apply HNC1 to the current goal.
We use p1 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
We will prove PNo_rel_strict_uniq_imv L R (ordsucc β) p1.
We will prove PNo_rel_strict_imv L R (ordsucc β) p1 ∧ ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc β) q → PNoEq_ (ordsucc β) p1 q.
Apply andI to the current goal.
An exact proof term for the current goal is Lp1imv.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R (ordsucc β) q.
We will prove PNoEq_ (ordsucc β) p1 q.
We prove the intermediate claim Lqb: PNo_rel_strict_imv L R β q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R (ordsucc β) Lsb q β (ordsuccI2 β) Hq.
We prove the intermediate claim Lpqe: PNoEq_ β p q.
An exact proof term for the current goal is Hp3 q Lqb.
Apply xm (q β) to the current goal.
Assume Hq1: q β.
We will prove PNoEq_ (ordsucc β) p1 q.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Apply ordsuccE β γ Hc to the current goal.
Assume H3: γ ∈ β.
We prove the intermediate claim Lpqce: p γ ↔ q γ.
An exact proof term for the current goal is Lpqe γ H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove p1 γ ↔ q γ.
Apply iffI to the current goal.
Assume H4: p γ ∨ γ = β.
Apply H4 to the current goal.
Assume H5: p γ.
An exact proof term for the current goal is Hpqc H5.
Assume H5: γ = β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H4: q γ.
We will prove p γ ∨ γ = β.
Apply orIL to the current goal.
We will prove p γ.
An exact proof term for the current goal is Hqpc H4.
Assume H3: γ = β.
We will prove p1 γ ↔ q γ.
Apply iffI to the current goal.
Assume _.
We will prove q γ.
rewrite the current goal using H3 (from left to right).
We will prove q β.
An exact proof term for the current goal is Hq1.
Assume H4: q γ.
We will prove p γ ∨ γ = β.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Assume Hq0: ¬ q β.
We will prove False.
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc β) p0.
Apply PNoEq_rel_strict_imv L R (ordsucc β) Lsb q p0 to the current goal.
We will prove PNoEq_ (ordsucc β) q p0.
Let γ be given.
Assume Hc: γ ∈ ordsucc β.
Apply ordsuccE β γ Hc to the current goal.
Assume H3: γ ∈ β.
We prove the intermediate claim Lpqce: p γ ↔ q γ.
An exact proof term for the current goal is Lpqe γ H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove q γ ↔ p0 γ.
Apply iffI to the current goal.
Assume H4: q γ.
We will prove p γ ∧ γ ≠ β.
Apply andI to the current goal.
We will prove p γ.
An exact proof term for the current goal is Hqpc H4.
We will prove γ ≠ β.
Assume H5: γ = β.
Apply In_irref β to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H4: p γ ∧ γ ≠ β.
Apply H4 to the current goal.
Assume H5 _.
An exact proof term for the current goal is Hpqc H5.
Assume H3: γ = β.
We will prove q γ ↔ p0 γ.
Apply iffI to the current goal.
Assume H4: q γ.
We will prove False.
Apply Hq0 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4.
Assume H4: p0 γ.
Apply H4 to the current goal.
Assume _ H5.
We will prove False.
Apply H5 to the current goal.
An exact proof term for the current goal is H3.
We will prove PNo_rel_strict_imv L R (ordsucc β) q.
An exact proof term for the current goal is Hq.
We will prove PNo_rel_strict_imv L R (ordsucc β) p1.
An exact proof term for the current goal is Lp1imv.
∎