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.
Let x3 of type ιο be given.
Let x4 of type ιο be given.
Assume H0: ordinal x1.
Assume H1: ordinal x2.
Assume H2: PNo_upc x0 x1 x3.
Assume H3: PNoLe x1 x3 x2 x4.
Apply H2 with PNo_upc x0 x2 x4.
Let x5 of type ι be given.
Assume H4: (λ x6 . and (ordinal x6) (∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x6 x7 x1 x3))) x5.
Apply H4 with PNo_upc x0 x2 x4.
Assume H5: ordinal x5.
Assume H6: ∃ x6 : ι → ο . and (x0 x5 x6) (PNoLe x5 x6 x1 x3).
Apply H6 with PNo_upc x0 x2 x4.
Let x6 of type ιο be given.
Assume H7: (λ x7 : ι → ο . and (x0 x5 x7) (PNoLe x5 x7 x1 x3)) x6.
Apply H7 with PNo_upc x0 x2 x4.
Assume H8: x0 x5 x6.
Assume H9: PNoLe x5 x6 x1 x3.
Let x7 of type ο be given.
Assume H10: ∀ x8 . and (ordinal x8) (∃ x9 : ι → ο . and (x0 x8 x9) (PNoLe x8 x9 x2 x4))x7.
Apply H10 with x5.
Apply andI with ordinal x5, ∃ x8 : ι → ο . and (x0 x5 x8) (PNoLe x5 x8 x2 x4) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x8 of type ο be given.
Assume H11: ∀ x9 : ι → ο . and (x0 x5 x9) (PNoLe x5 x9 x2 x4)x8.
Apply H11 with x6.
Apply andI with x0 x5 x6, PNoLe x5 x6 x2 x4 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply PNoLe_tra with x5, x1, x2, x6, x3, x4 leaving 5 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
The subproof is completed by applying H3.