Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x2 ∈ setsum x0 x1.
Claim L1: ordinal (binunion (9d271.. x0) (9d271.. x1))
Apply ordinal_binunion with 9d271.. x0, 9d271.. x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_1ec7349a6007c1951cbc9535ca5769b83316f6778bed19ab211854c4c6028c5d with x0.
The subproof is completed by applying unknownprop_1ec7349a6007c1951cbc9535ca5769b83316f6778bed19ab211854c4c6028c5d with x1.
Apply setsum_Inj_inv with x0, x1, x2, x2 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H2: ∃ x3 . and (x3 ∈ x0) (x2 = Inj0 x3).
Apply H2 with x2 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Let x3 of type ι be given.
Assume H3: (λ x4 . and (x4 ∈ x0) (x2 = Inj0 x4)) x3.
Apply H3 with x2 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Assume H4: x3 ∈ x0.
Assume H5: x2 = Inj0 x3.
Apply H5 with λ x4 x5 . x5 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Apply V_I with Inj0 x3, ordsucc (9d271.. x3), ordsucc (binunion (9d271.. x0) (9d271.. x1)) leaving 2 subgoals.
Apply ordinal_ordsucc_In with binunion (9d271.. x0) (9d271.. x1), 9d271.. x3 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply binunionI1 with 9d271.. x0, 9d271.. x1, 9d271.. x3.
Apply unknownprop_24ba76162cbabacbe8136cf5d6f6295437383ecf4b3946427a5b4b7d60ed1941 with x3, x0.
The subproof is completed by applying H4.
The subproof is completed by applying unknownprop_c073b14b7a96e69e7e8f5a1fe3901014c36ac527c42f83bf6876840b11d83588 with x3.
Assume H2: ∃ x3 . and (x3 ∈ x1) (x2 = Inj1 x3).
Apply H2 with x2 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Let x3 of type ι be given.
Assume H3: (λ x4 . and (x4 ∈ x1) (x2 = Inj1 x4)) x3.
Apply H3 with x2 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Assume H4: x3 ∈ x1.
Assume H5: x2 = Inj1 x3.
Apply H5 with λ x4 x5 . x5 ∈ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))).
Apply V_I with Inj1 x3, ordsucc (9d271.. x3), ordsucc (binunion (9d271.. x0) (9d271.. x1)) leaving 2 subgoals.
Apply ordinal_ordsucc_In with binunion (9d271.. x0) (9d271.. x1), 9d271.. x3 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply binunionI2 with 9d271.. x0, 9d271.. x1, 9d271.. x3.
Apply unknownprop_24ba76162cbabacbe8136cf5d6f6295437383ecf4b3946427a5b4b7d60ed1941 with x3, x1.
The subproof is completed by applying H4.
The subproof is completed by applying unknownprop_7520792d9c4001bd88f3e8a251d89ba23341c4c0a08e5856d9d9558b1998ce5c with x3.
■