Let α be given.
Assume Ha: ordinal α.
Let p be given.
Let β be given.
Assume Hb: β ∈ α.
We will prove β ∈ PSNo α p ↔ p β.
Apply iffI to the current goal.
Assume H1: β ∈ {β ∈ α|p β} ∪ {β '|β ∈ α, ¬ p β}.
Apply binunionE {β ∈ α|p β} {β '|β ∈ α, ¬ p β} β H1 to the current goal.
Assume H2: β ∈ {β ∈ α|p β}.
An exact proof term for the current goal is SepE2 α p β H2.
Assume H2: β ∈ {β '|β ∈ α, ¬ p β}.
We will prove False.
Apply ReplSepE_impred α (λβ ⇒ ¬ p β) (λx ⇒ x ') β H2 to the current goal.
Let γ be given.
Assume Hc: γ ∈ α.
Assume H3: ¬ p γ.
Assume H4: β = γ '.
Apply tagged_notin_ordinal α γ Ha to the current goal.
We will prove γ ' ∈ α.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb.
Assume H1: p β.
We will prove β ∈ PSNo α p.
We will prove β ∈ {β ∈ α|p β} ∪ {β '|β ∈ α, ¬ p β}.
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.
∎