Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: ordinal x0.

Assume H1: In x0 (Repl x1 (λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2)).

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x1, λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2, x0, False leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: In x2 x1.

Assume H3: x0 = (λ x3 . SetAdjoin x3 (Sing 1)) x2.

Apply unknownprop_0016de04f44a712243c9eeee572a992709374894dd4f8741b2a55208a71b7c48 with x2.

Apply H3 with λ x3 x4 . ordinal x3.

The subproof is completed by applying H0.

■

Proofgold Proof