Let α be given.
Assume Ha.
Let p be given.
We will prove PSNo α p ⊆ SNoElts_ α ∧ ∀β ∈ α, exactly1of2 (β ' ∈ PSNo α p) (β ∈ PSNo α p).
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ PSNo α p.
We will prove u ∈ SNoElts_ α.
Apply binunionE {β ∈ α|p β} {β '|β ∈ α, ¬ p β} u Hu to the current goal.
Assume H1: u ∈ {β ∈ α|p β}.
Apply SepE α p u H1 to the current goal.
Assume H2: u ∈ α.
Assume H3: p u.
We will prove u ∈ α ∪ {β '|β ∈ α}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is H2.
Assume H1: u ∈ {β '|β ∈ α, ¬ p β}.
Apply ReplSepE_impred α (λβ ⇒ ¬ p β) (λβ ⇒ β ') u H1 to the current goal.
Let β be given.
Assume H2: β ∈ α.
Assume H3: ¬ p β.
Assume H4: u = β '.
We will prove u ∈ α ∪ {β '|β ∈ α}.
Apply binunionI2 to the current goal.
We will prove u ∈ {β '|β ∈ α}.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is ReplI α (λβ ⇒ β ') β H2.
Let β be given.
Assume H1: β ∈ α.
We prove the intermediate claim Lbeta: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β H1.
We will prove exactly1of2 (β ' ∈ PSNo α p) (β ∈ PSNo α p).
Apply xm (p β) to the current goal.
Assume H2: p β.
Apply exactly1of2_I2 to the current goal.
We will prove β ' ∉ PSNo α p.
Assume H3: β ' ∈ PSNo α p.
Apply binunionE {β ∈ α|p β} {β '|β ∈ α, ¬ p β} (β ') H3 to the current goal.
Assume H4: β ' ∈ {β ∈ α|p β}.
Apply SepE α p (β ') H4 to the current goal.
Assume H5: β ' ∈ α.
Assume H6: p (β ').
We will prove False.
Apply tagged_not_ordinal β to the current goal.
An exact proof term for the current goal is ordinal_Hered α Ha (β ') H5.
Assume H4: β ' ∈ {β '|β ∈ α, ¬ p β}.
Apply ReplSepE_impred α (λβ ⇒ ¬ p β) (λβ ⇒ β ') (β ') H4 to the current goal.
Let γ be given.
Assume H5: γ ∈ α.
Assume H6: ¬ p γ.
Assume H7: β ' = γ '.
We prove the intermediate claim Lgamma: ordinal γ.
An exact proof term for the current goal is ordinal_Hered α Ha γ H5.
We prove the intermediate claim L1: β = γ.
An exact proof term for the current goal is tagged_eqE_eq β γ Lbeta Lgamma H7.
Apply H6 to the current goal.
We will prove p γ.
rewrite the current goal using L1 (from right to left).
We will prove p β.
An exact proof term for the current goal is H2.
We will prove β ∈ {β ∈ α|p β} ∪ {β '|β ∈ α, ¬ p β}.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is SepI α p β H1 H2.
Assume H2: ¬ p β.
Apply exactly1of2_I1 to the current goal.
We will prove β ' ∈ {β ∈ α|p β} ∪ {β '|β ∈ α, ¬ p β}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is ReplSepI α (λβ ⇒ ¬ p β) (λβ ⇒ β ') β H1 H2.
We will prove β ∉ PSNo α p.
Assume H3: β ∈ PSNo α p.
Apply binunionE {β ∈ α|p β} {β '|β ∈ α, ¬ p β} β H3 to the current goal.
Assume H4: β ∈ {β ∈ α|p β}.
Apply SepE α p β H4 to the current goal.
Assume H5: β ∈ α.
Assume H6: p β.
We will prove False.
An exact proof term for the current goal is H2 H6.
Assume H4: β ∈ {β '|β ∈ α, ¬ p β}.
Apply ReplSepE_impred α (λβ ⇒ ¬ p β) (λβ ⇒ β ') β H4 to the current goal.
Let γ be given.
Assume H5: γ ∈ α.
Assume H6: ¬ p γ.
Assume H7: β = γ '.
Apply tagged_not_ordinal γ to the current goal.
We will prove ordinal (γ ').
rewrite the current goal using H7 (from right to left).
An exact proof term for the current goal is Lbeta.
∎