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