Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Assume H2: In ((λ x2 . SetAdjoin x2 (Sing 1)) x1) (Repl x0 (λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x0, λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2, (λ x2 . SetAdjoin x2 (Sing 1)) x1, In x1 x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3: In x2 x0.
Assume H4: (λ x3 . SetAdjoin x3 (Sing 1)) x1 = (λ x3 . SetAdjoin x3 (Sing 1)) x2.
Claim L5: x1 = x2
Apply unknownprop_b1443874f1d94e8ae4702eeac0a8d34b82a3a5fa428acb67206d58ef176d9733 with x1, x2 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply L5 with λ x3 x4 . In x4 x0.
The subproof is completed by applying H3.
■