Let α, β and γ be given.
Assume Ha Hb Hc.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hc to the current goal.
Assume Hc1 _.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE α β p q Hpq to the current goal.
Assume Hpq1: PNoLt_ (α ∩ β) p q.
Apply Hpq1 to the current goal.
Let δ be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: δ ∈ α ∩ β.
Apply binintersectE α β δ Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ δ p q.
Assume Hpq4: ¬ p δ.
Assume Hpq5: q δ.
We prove the intermediate claim Ld: ordinal δ.
An exact proof term for the current goal is ordinal_Hered β Hb δ Hd2.
Apply PNoLtE β γ q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (β ∩ γ) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ β ∩ γ.
Apply binintersectE β γ eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered β Hb eps He1.
We will prove PNoLt α p γ r.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
Apply ordinal_trichotomy_or δ eps Ld Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: δ ∈ eps.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ α ∩ γ.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove δ ∈ γ.
An exact proof term for the current goal is Hc1 eps He2 δ H1.
Apply and3I to the current goal.
We will prove PNoEq_ δ p r.
Apply PNoEq_tra_ δ p q r to the current goal.
We will prove PNoEq_ δ p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ δ q r.
Apply PNoEq_antimon_ q r eps Le δ H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p δ.
An exact proof term for the current goal is Hpq4.
We will prove r δ.
An exact proof term for the current goal is iffEL (q δ) (r δ) (Hqr3 δ H1) Hpq5.
Assume H1: δ = eps.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ α ∩ γ.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove δ ∈ γ.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ δ p r.
Apply PNoEq_tra_ δ p q r to the current goal.
We will prove PNoEq_ δ p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ δ q r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr3.
We will prove ¬ p δ.
An exact proof term for the current goal is Hpq4.
We will prove r δ.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ δ.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ α ∩ γ.
Apply binintersectI to the current goal.
We will prove eps ∈ α.
An exact proof term for the current goal is Ha1 δ Hd1 eps H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q δ Ld eps H1 to the current goal.
We will prove PNoEq_ δ p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq3 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: β ∈ γ.
Assume Hqr2: PNoEq_ β q r.
Assume Hqr3: r β.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ α ∩ γ.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove δ ∈ γ.
An exact proof term for the current goal is Hc1 β Hqr1 δ Hd2.
Apply and3I to the current goal.
We will prove PNoEq_ δ p r.
Apply PNoEq_tra_ δ p q r to the current goal.
We will prove PNoEq_ δ p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ δ q r.
Apply PNoEq_antimon_ q r β Hb δ Hd2 to the current goal.
We will prove PNoEq_ β q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p δ.
An exact proof term for the current goal is Hpq4.
We will prove r δ.
An exact proof term for the current goal is iffEL (q δ) (r δ) (Hqr2 δ Hd2) Hpq5.
Assume Hqr1: γ ∈ β.
Assume Hqr2: PNoEq_ γ q r.
Assume Hqr3: ¬ q γ.
Apply ordinal_trichotomy_or δ γ Ld Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: δ ∈ γ.
We will prove PNoLt α p γ r.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
We use δ to witness the existential quantifier.
Apply andI to the current goal.
We will prove δ ∈ α ∩ γ.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove δ ∈ γ.
An exact proof term for the current goal is H1.
Apply and3I to the current goal.
We will prove PNoEq_ δ p r.
Apply PNoEq_tra_ δ p q r to the current goal.
We will prove PNoEq_ δ p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ δ q r.
Apply PNoEq_antimon_ q r γ Hc δ H1 to the current goal.
We will prove PNoEq_ γ q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p δ.
An exact proof term for the current goal is Hpq4.
We will prove r δ.
An exact proof term for the current goal is iffEL (q δ) (r δ) (Hqr2 δ H1) Hpq5.
Assume H1: δ = γ.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ α.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hd1.
We will prove PNoEq_ γ p r.
Apply PNoEq_tra_ γ p q r to the current goal.
We will prove PNoEq_ γ p q.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ γ q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p γ.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq4.
Assume H1: γ ∈ δ.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ α.
An exact proof term for the current goal is Ha1 δ Hd1 γ H1.
We will prove PNoEq_ γ p r.
Apply PNoEq_tra_ γ p q r to the current goal.
We will prove PNoEq_ γ p q.
Apply PNoEq_antimon_ p q δ Ld γ H1 to the current goal.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ γ q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p γ.
Assume H2: p γ.
Apply Hqr3 to the current goal.
We will prove q γ.
An exact proof term for the current goal is iffEL (p γ) (q γ) (Hpq3 γ H1) H2.
Assume Hpq1: α ∈ β.
Assume Hpq2: PNoEq_ α p q.
Assume Hpq3: q α.
Apply PNoLtE β γ q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (β ∩ γ) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ β ∩ γ.
Apply binintersectE β γ eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered β Hb eps He1.
Apply ordinal_trichotomy_or α eps Ha Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: α ∈ eps.
We will prove PNoLt α p γ r.
Apply PNoLtI2 to the current goal.
We will prove α ∈ γ.
An exact proof term for the current goal is Hc1 eps He2 α H1.
We will prove PNoEq_ α p r.
Apply PNoEq_tra_ α p q r to the current goal.
We will prove PNoEq_ α p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ α q r.
Apply PNoEq_antimon_ q r eps Le α H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r α.
An exact proof term for the current goal is iffEL (q α) (r α) (Hqr3 α H1) Hpq3.
Assume H1: α = eps.
We will prove PNoLt α p γ r.
Apply PNoLtI2 to the current goal.
We will prove α ∈ γ.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
We will prove PNoEq_ α p r.
Apply PNoEq_tra_ α p q r to the current goal.
We will prove PNoEq_ α p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ α q r.
rewrite the current goal using H1 (from left to right).
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r α.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ α.
We will prove PNoLt α p γ r.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ α ∩ γ.
Apply binintersectI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q α Ha eps H1 to the current goal.
We will prove PNoEq_ α p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: β ∈ γ.
Assume Hqr2: PNoEq_ β q r.
Assume Hqr3: r β.
Apply PNoLtI2 to the current goal.
We will prove α ∈ γ.
An exact proof term for the current goal is Hc1 β Hqr1 α Hpq1.
We will prove PNoEq_ α p r.
Apply PNoEq_tra_ α p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r β Hb α Hpq1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r α.
An exact proof term for the current goal is iffEL (q α) (r α) (Hqr2 α Hpq1) Hpq3.
Assume Hqr1: γ ∈ β.
Assume Hqr2: PNoEq_ γ q r.
Assume Hqr3: ¬ q γ.
We will prove PNoLt α p γ r.
Apply ordinal_trichotomy_or α γ Ha Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: α ∈ γ.
Apply PNoLtI2 to the current goal.
We will prove α ∈ γ.
An exact proof term for the current goal is H1.
We will prove PNoEq_ α p r.
Apply PNoEq_tra_ α p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r γ Hc α H1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r α.
An exact proof term for the current goal is iffEL (q α) (r α) (Hqr2 α H1) Hpq3.
Assume H1: α = γ.
We will prove False.
Apply Hqr3 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
Assume H1: γ ∈ α.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ α.
An exact proof term for the current goal is H1.
We will prove PNoEq_ γ p r.
Apply PNoEq_tra_ γ p q r to the current goal.
Apply PNoEq_antimon_ p q α Ha γ H1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p γ.
Assume H2: p γ.
Apply Hqr3 to the current goal.
We will prove q γ.
An exact proof term for the current goal is iffEL (p γ) (q γ) (Hpq2 γ H1) H2.
Assume Hpq1: β ∈ α.
Assume Hpq2: PNoEq_ β p q.
Assume Hpq3: ¬ p β.
Apply PNoLtE β γ q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (β ∩ γ) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ β ∩ γ.
Apply binintersectE β γ eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We will prove PNoLt α p γ r.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ α ∩ γ.
Apply binintersectI to the current goal.
We will prove eps ∈ α.
An exact proof term for the current goal is Ha1 β Hpq1 eps He1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q β Hb eps He1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H1: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps He1) H1.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: β ∈ γ.
Assume Hqr2: PNoEq_ β q r.
Assume Hqr3: r β.
Apply PNoLtI1 to the current goal.
We will prove ∃δ ∈ α ∩ γ, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.
We use β to witness the existential quantifier.
Apply andI to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hpq1.
An exact proof term for the current goal is Hqr1.
Apply and3I to the current goal.
Apply PNoEq_tra_ β p q r to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p β.
An exact proof term for the current goal is Hpq3.
We will prove r β.
An exact proof term for the current goal is Hqr3.
Assume Hqr1: γ ∈ β.
Assume Hqr2: PNoEq_ γ q r.
Assume Hqr3: ¬ q γ.
Apply PNoLtI3 to the current goal.
We will prove γ ∈ α.
An exact proof term for the current goal is Ha1 β Hpq1 γ Hqr1.
We will prove PNoEq_ γ p r.
Apply PNoEq_tra_ γ p q r to the current goal.
We will prove PNoEq_ γ p q.
Apply PNoEq_antimon_ p q β Hb γ Hqr1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p γ.
Assume H1: p γ.
Apply Hqr3 to the current goal.
We will prove q γ.
An exact proof term for the current goal is iffEL (p γ) (q γ) (Hpq2 γ Hqr1) H1.
∎