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 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 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.