Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal ((λ x1 . SetAdjoin x1 (Sing 1)) x0).
Claim L1: Sing 1 ∈ (λ x1 . SetAdjoin x1 (Sing 1)) x0
Apply binunionI2 with x0, Sing (Sing 1), Sing 1.
The subproof is completed by applying SingI with Sing 1.
Apply not_ordinal_Sing1.
Apply ordinal_Hered with (λ x1 . SetAdjoin x1 (Sing 1)) x0, Sing 1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L1.
■