Let alpha be given.
Assume Ha: ordinal alpha.
Let p be given.
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove beta ∈ PSNo alpha p ↔ p beta.
Apply iffI to the current goal.
Assume H1: beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.
Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} beta H1 to the current goal.
Assume H2: beta ∈ {beta ∈ alpha|p beta}.
An exact proof term for the current goal is SepE2 alpha p beta H2.
Assume H2: beta ∈ {beta '|beta ∈ alpha, ¬ p beta}.
We will prove False.
Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λx ⇒ x ') beta H2 to the current goal.
Let gamma be given.
Assume Hc: gamma ∈ alpha.
Assume H3: ¬ p gamma.
Assume H4: beta = gamma '.
Apply tagged_notin_ordinal alpha gamma Ha to the current goal.
We will prove gamma ' ∈ alpha.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb.
Assume H1: p beta.
We will prove beta ∈ PSNo alpha p.
We will prove beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.
Apply binunionI1 to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is H1.
∎