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