Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: PNoLt (SNoLev x) (λβ ⇒ β ∈ x) (SNoLev y) (λβ ⇒ β ∈ y).
Let p be given.
Assume Hp1 Hp2 Hp3.
We prove the intermediate claim LLx: ordinal (SNoLev x).
Apply SNoLev_ordinal x to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim LLy: ordinal (SNoLev y).
Apply SNoLev_ordinal y to the current goal.
An exact proof term for the current goal is Hy.
Apply PNoLtE (SNoLev x) (SNoLev y) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) Hxy to the current goal.
Assume H1: PNoLt_ (SNoLev x ∩ SNoLev y) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
Apply PNoLt_E_ (SNoLev x ∩ SNoLev y) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) H1 to the current goal.
Let α be given.
Assume Ha: α ∈ SNoLev x ∩ SNoLev y.
Assume H2: PNoEq_ α (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
Assume H3: α ∉ x.
Assume H4: α ∈ y.
Apply binintersectE (SNoLev x) (SNoLev y) α Ha to the current goal.
Assume Ha1: α ∈ SNoLev x.
Assume Ha2: α ∈ SNoLev y.
We prove the intermediate claim La: ordinal α.
An exact proof term for the current goal is ordinal_Hered (SNoLev x) LLx α Ha1.
Set z to be the term PSNo α (λβ ⇒ β ∈ x).
We prove the intermediate claim L1: SNo_ α z.
Apply SNo_PSNo to the current goal.
An exact proof term for the current goal is La.
We prove the intermediate claim L2: SNo z.
We will prove ∃α, ordinal α ∧ SNo_ α z.
We use α to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is La.
An exact proof term for the current goal is L1.
Apply SNoLev_prop z L2 to the current goal.
Assume Hz1: ordinal (SNoLev z).
Assume Hz2: SNo_ (SNoLev z) z.
We prove the intermediate claim L3: SNoLev z = α.
An exact proof term for the current goal is SNoLev_uniq z (SNoLev z) α Hz1 La Hz2 L1.
We prove the intermediate claim L4: SNoEq_ α z x.
We will prove PNoEq_ α (λβ ⇒ β ∈ z) (λβ ⇒ β ∈ x).
We will prove PNoEq_ α (λβ ⇒ β ∈ PSNo α (λβ ⇒ β ∈ x)) (λβ ⇒ β ∈ x).
Apply PNoEq_PSNo to the current goal.
An exact proof term for the current goal is La.
We prove the intermediate claim L5: SNoEq_ α z y.
Apply SNoEq_tra_ α z x y L4 to the current goal.
We will prove SNoEq_ α x y.
We will prove PNoEq_ α (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
An exact proof term for the current goal is H2.
Apply Hp1 z L2 to the current goal.
We will prove SNoLev z ∈ SNoLev x ∩ SNoLev y.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is Ha.
We will prove SNoEq_ (SNoLev z) z x.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L4.
We will prove SNoEq_ (SNoLev z) z y.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L5.
We will prove x < z.
We will prove PNoLt (SNoLev x) (λβ ⇒ β ∈ x) (SNoLev z) (λβ ⇒ β ∈ z).
rewrite the current goal using L3 (from left to right).
We will prove PNoLt (SNoLev x) (λβ ⇒ β ∈ x) α (λβ ⇒ β ∈ z).
Apply PNoLtI3 to the current goal.
We will prove α ∈ SNoLev x.
An exact proof term for the current goal is Ha1.
We will prove PNoEq_ α (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ z).
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is L4.
We will prove α ∉ x.
An exact proof term for the current goal is H3.
We will prove z < y.
We will prove PNoLt (SNoLev z) (λβ ⇒ β ∈ z) (SNoLev y) (λβ ⇒ β ∈ y).
rewrite the current goal using L3 (from left to right).
We will prove PNoLt α (λβ ⇒ β ∈ z) (SNoLev y) (λβ ⇒ β ∈ y).
Apply PNoLtI2 to the current goal.
We will prove α ∈ SNoLev y.
An exact proof term for the current goal is Ha2.
We will prove PNoEq_ α (λβ ⇒ β ∈ z) (λβ ⇒ β ∈ y).
An exact proof term for the current goal is L5.
We will prove α ∈ y.
An exact proof term for the current goal is H4.
We will prove SNoLev z ∉ x.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H3.
We will prove SNoLev z ∈ y.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H4.
Assume H1: SNoLev x ∈ SNoLev y.
Assume H2: PNoEq_ (SNoLev x) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
Assume H3: SNoLev x ∈ y.
Apply Hp2 to the current goal.
We will prove SNoLev x ∈ SNoLev y.
An exact proof term for the current goal is H1.
We will prove SNoEq_ (SNoLev x) x y.
An exact proof term for the current goal is H2.
We will prove SNoLev x ∈ y.
An exact proof term for the current goal is H3.
Assume H1: SNoLev y ∈ SNoLev x.
Assume H2: PNoEq_ (SNoLev y) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
Assume H3: SNoLev y ∉ x.
Apply Hp3 to the current goal.
We will prove SNoLev y ∈ SNoLev x.
An exact proof term for the current goal is H1.
We will prove SNoEq_ (SNoLev y) x y.
An exact proof term for the current goal is H2.
We will prove SNoLev y ∉ x.
An exact proof term for the current goal is H3.
∎