Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: atleastp (ordsucc x0) x1.
Assume H2: ∀ x2 . x2x1ordinal x2.
Let x2 of type ο be given.
Assume H3: ∀ x3 x4 . equip x0 x3x4x1x3x1x3x4x2.
Apply unknownprop_b3e91047f76692c2df7eb5955e15ae636bf411ce8b2adc37d0ed519e38c03c5e with ordsucc x0, x1, x2 leaving 4 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ιι be given.
Assume H4: (λ x4 : ι → ι . and (inj (ordsucc x0) x1 x4) (∀ x5 . x5ordsucc x0∀ x6 . x6x5x4 x6x4 x5)) x3.
Apply H4 with x2.
Assume H5: inj (ordsucc x0) x1 x3.
Assume H6: ∀ x4 . x4ordsucc x0∀ x5 . x5x4x3 x5x3 x4.
Apply H5 with x2.
Assume H7: ∀ x4 . x4ordsucc x0x3 x4x1.
Assume H8: ∀ x4 . x4ordsucc x0∀ x5 . x5ordsucc x0x3 x4 = x3 x5x4 = x5.
Apply H3 with {x3 x4|x4 ∈ x0}, x3 x0 leaving 4 subgoals.
Apply unknownprop_6f924010899e62355200d41f1cef23d6373bef28ff540d0bdb872dcb6e86d39f with x0, x3.
Let x4 of type ι be given.
Assume H9: x4x0.
Let x5 of type ι be given.
Assume H10: x5x0.
Apply H8 with x4, x5 leaving 2 subgoals.
Apply ordsuccI1 with x0, x4.
The subproof is completed by applying H9.
Apply ordsuccI1 with x0, x5.
The subproof is completed by applying H10.
Apply H7 with x0.
The subproof is completed by applying ordsuccI2 with x0.
Let x4 of type ι be given.
Assume H9: x4{x3 x5|x5 ∈ x0}.
Apply ReplE_impred with x0, x3, x4, x4x1 leaving 2 subgoals.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H10: x5x0.
Assume H11: x4 = x3 x5.
Apply H11 with λ x6 x7 . x7x1.
Apply H7 with x5.
Apply ordsuccI1 with x0, x5.
The subproof is completed by applying H10.
Let x4 of type ι be given.
Assume H9: x4{x3 x5|x5 ∈ x0}.
Apply ReplE_impred with x0, x3, x4, x4x3 x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H10: x5x0.
Assume H11: x4 = x3 x5.
Apply H11 with λ x6 x7 . x7x3 x0.
Apply H6 with x0, x5 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x0.
The subproof is completed by applying H10.