Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply H0 with
PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Assume H2:
∀ x3 . x3 ∈ x2 ⟶ TransSet x3.
Let x3 of type ι → ο be given.
Apply H5 with
PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)).
Apply andI with
PNo_rel_strict_upperbd x0 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)),
PNo_rel_strict_lowerbd x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)) leaving 2 subgoals.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Apply H11 with
PNoLt x4 x5 (ordsucc x2) (λ x6 . and (x3 x6) (x6 = x2 ⟶ ∀ x7 : ο . x7)).
Let x6 of type ι be given.
Assume H13:
(λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (PNoLe x4 x5 x7 x8))) x6.
Apply H13 with
PNoLt x4 x5 (ordsucc x2) (λ x7 . and (x3 x7) (x7 = x2 ⟶ ∀ x8 : ο . x8)).
Assume H15:
∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x4 x5 x6 x7).
Apply H15 with
PNoLt x4 x5 (ordsucc x2) (λ x7 . and (x3 x7) (x7 = x2 ⟶ ∀ x8 : ο . x8)).
Let x7 of type ι → ο be given.
Assume H16:
(λ x8 : ι → ο . and (x0 x6 x8) (PNoLe x4 x5 x6 x8)) x7.
Apply H16 with
PNoLt x4 x5 (ordsucc x2) (λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9)).
Assume H17: x0 x6 x7.
Assume H18:
PNoLe x4 x5 x6 x7.
Apply PNoLeLt_tra with
x4,
x6,
ordsucc x2,
x5,
x7,
λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying L8.
The subproof is completed by applying H18.
Apply PNoLt_trichotomy_or with
x6,
ordsucc x2,
x7,
λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9),
PNoLt x6 x7 (ordsucc x2) (λ x8 . and (x3 x8) (x8 = x2 ⟶ ∀ x9 : ο . x9)) leaving 4 subgoals.
The subproof is completed by applying H14.