Search for blocks/addresses/...

Proofgold Proof

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