Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Apply least_ordinal_ex with
λ x3 . ∃ x4 : ι → ο . 47618.. x0 x1 x3 x4.
Apply unknownprop_13deec40494b47380fd1941c6a625d447cd8171018141d4d3bc740ca96c35ef7 with
x0,
x1,
x2,
∃ x3 . and (ordinal x3) (∃ x4 : ι → ο . 47618.. x0 x1 x3 x4) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply L4 with
∃ x3 . ∃ x4 : ι → ο . 1a487.. x0 x1 x3 x4.
Let x3 of type ι be given.
Apply H5 with
∃ x4 . ∃ x5 : ι → ο . 1a487.. x0 x1 x4 x5.
Apply H6 with
(∀ x4 . prim1 x4 x3 ⟶ not (∃ x5 : ι → ο . 47618.. x0 x1 x4 x5)) ⟶ ∃ x4 . ∃ x5 : ι → ο . 1a487.. x0 x1 x4 x5.
Assume H8:
∃ x4 : ι → ο . 47618.. x0 x1 x3 x4.
Apply H8 with
∃ x4 . ∃ x5 : ι → ο . 1a487.. x0 x1 x4 x5.
Let x4 of type ι → ο be given.
Let x5 of type ο be given.
Assume H11:
∀ x6 . (∃ x7 : ι → ο . 1a487.. x0 x1 x6 x7) ⟶ x5.
Apply H11 with
x3.
Let x6 of type ο be given.
Assume H12:
∀ x7 : ι → ο . 1a487.. x0 x1 x3 x7 ⟶ x6.
Apply H12 with
x4.
Apply and3I with
ordinal x3,
47618.. x0 x1 x3 x4,
∀ x7 . prim1 x7 x3 ⟶ ∀ x8 : ι → ο . not (47618.. x0 x1 x7 x8) leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
Let x7 of type ι be given.
Let x8 of type ι → ο be given.
Apply H9 with
x7 leaving 2 subgoals.
The subproof is completed by applying H13.
Let x9 of type ο be given.
Assume H15:
∀ x10 : ι → ο . 47618.. x0 x1 x7 x10 ⟶ x9.
Apply H15 with
x8.
The subproof is completed by applying H14.