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: x4 ∈ x2.
Let x5 of type ι → ο be given.
Apply H0 with
PNoLt x2 x3 x4 x5.
Assume H6:
∀ x6 . x6 ∈ x1 ⟶ TransSet x6.
Apply H4 with
PNoLt x2 x3 x4 x5.
Let x6 of type ι be given.
Assume H12:
(λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (PNoLe x7 x8 x4 x5))) x6.
Apply H12 with
PNoLt x2 x3 x4 x5.
Assume H14:
∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x6 x7 x4 x5).
Apply H14 with
PNoLt x2 x3 x4 x5.
Let x7 of type ι → ο be given.
Assume H15:
(λ x8 : ι → ο . and (x0 x6 x8) (PNoLe x6 x8 x4 x5)) x7.
Apply H15 with
PNoLt x2 x3 x4 x5.
Assume H16: x0 x6 x7.
Assume H17:
PNoLe x6 x7 x4 x5.
Apply PNoLt_trichotomy_or with
x4,
x2,
x5,
x3,
PNoLt x2 x3 x4 x5 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L8.
Apply H22 with
PNoLt x2 x3 x4 x5 leaving 2 subgoals.
Assume H23:
PNoLt x4 x5 x2 x3.
Apply FalseE with
PNoLt x2 x3 x4 x5.
Apply PNoLtE with
x4,
x2,
x5,
x3,
False leaving 4 subgoals.
The subproof is completed by applying H23.
Apply binintersect_Subq_eq_1 with
x4,
x2,
λ x8 x9 . PNoLt_ x9 x5 x3 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L11.
Apply H24 with
False.
Apply PNoLt_irref with
x1,
x3,
∀ x8 . (λ x9 . and (x9 ∈ x4) (and (and (PNoEq_ x9 x5 x3) (not (x5 x9))) (x3 x9))) x8 ⟶ False.
Apply PNoLt_tra with
x1,
x4,
x1,
x3,
x5,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.
The subproof is completed by applying H0.
The subproof is completed by applying L19.
Apply PNoLtI1 with
x4,
x1,
x5,
x3.
Apply binintersect_Subq_eq_1 with
x4,
x1,
λ x8 x9 . PNoLt_ x9 x5 x3 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying H24.
Assume H24: x4 ∈ x2.
Assume H26: x3 x4.
Apply PNoLt_irref with
x1,
x3.
Apply PNoLt_tra with
x1,
x4,
x1,
x3,
x5,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.
The subproof is completed by applying H0.
The subproof is completed by applying L19.
Apply PNoLtI2 with
x4,
x1,
x5,
x3 leaving 3 subgoals.
The subproof is completed by applying L20.
The subproof is completed by applying H25.
The subproof is completed by applying H26.
Assume H24: x2 ∈ x4.
Apply FalseE with
PNoEq_ x2 x5 x3 ⟶ not (x5 x2) ⟶ False.
Apply In_no2cycle with
x2,
x4 leaving 2 subgoals.
The subproof is completed by applying H24.
The subproof is completed by applying H3.
Apply H23 with
PNoLt x2 x3 x4 x5.
Assume H24: x4 = x2.
Apply FalseE with
... ⟶ PNoLt x2 x3 ... ....