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.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Assume H2: 40dde.. x0 x2 x1 x3.
Assume H3: PNoEq_ x1 x3 x4.
Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x0, x1, x2, x3, 40dde.. x0 x2 x1 x4 leaving 4 subgoals.
The subproof is completed by applying H2.
Assume H4: PNoLt_ (d3786.. x0 x1) x2 x3.
Apply H4 with 40dde.. x0 x2 x1 x4.
Let x5 of type ι be given.
Assume H5: (λ x6 . and (prim1 x6 (d3786.. x0 x1)) (and (and (PNoEq_ x6 x2 x3) (not (x2 x6))) (x3 x6))) x5.
Apply H5 with 40dde.. x0 x2 x1 x4.
Assume H6: prim1 x5 (d3786.. x0 x1).
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x0, x1, x5, and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5) ⟶ 40dde.. x0 x2 x1 x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: prim1 x5 x0.
Assume H8: prim1 x5 x1.
Assume H9: and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5).
Apply H9 with 40dde.. x0 x2 x1 x4.
Assume H10: and (PNoEq_ x5 x2 x3) (not (x2 x5)).
Apply H10 with x3 x5 ⟶ 40dde.. x0 x2 x1 x4.
Assume H11: PNoEq_ x5 x2 x3.
Assume H12: not (x2 x5).
Assume H13: x3 x5.
Apply unknownprop_ac970f51deca19d20e9a8350c3518ea802533ebd2768fe799c9b97ea3dd03596 with x0, x1, x2, x4.
Let x6 of type ο be given.
Assume H14: ∀ x7 . and (prim1 x7 (d3786.. x0 x1)) (and (and (PNoEq_ x7 x2 x4) (not (x2 x7))) (x4 x7)) ⟶ x6.
Apply H14 with x5.
Apply andI with prim1 x5 (d3786.. x0 x1), and (and (PNoEq_ x5 x2 x4) (not (x2 x5))) (x4 x5) leaving 2 subgoals.
The subproof is completed by applying H6.
Apply and3I with PNoEq_ x5 x2 x4, not (x2 x5), x4 x5 leaving 3 subgoals.
Apply PNoEq_tra_ with x5, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply PNoEq_antimon_ with x3, x4, x1, x5 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H8.
The subproof is completed by applying H3.
The subproof is completed by applying H12.
Apply iffEL with x3 x5, x4 x5 leaving 2 subgoals.
Apply H3 with x5.
The subproof is completed by applying H8.
The subproof is completed by applying H13.
Assume H4: prim1 x0 x1.
Assume H5: PNoEq_ x0 x2 x3.
Assume H6: x3 x0.
Apply unknownprop_9bcd3ca68066c7069c00444b0b53fe3ae6267cb29974000b72e5fe8327360c0b with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply PNoEq_tra_ with x0, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply PNoEq_antimon_ with x3, x4, x1, x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Apply iffEL with x3 x0, x4 x0 leaving 2 subgoals.
Apply H3 with x0.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Assume H4: prim1 x1 x0.
Assume H5: PNoEq_ x1 x2 x3.
Assume H6: not (x2 x1).
Apply unknownprop_b51c738b3a14385af55eef02a445728dc056a37996fdc42e5ede8e064af23c97 with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply PNoEq_tra_ with x1, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
■