Let x0 of type ι be given.
Assume H1:
∀ x1 . x1 ∈ x0 ⟶ ordinal x1.
Let x1 of type ο be given.
Assume H2: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x3 ⟶ x3 ∈ x4 ⟶ (∀ x5 . x5 ∈ x0 ⟶ ∀ x6 : ι → ο . x6 x2 ⟶ x6 x3 ⟶ x6 x4 ⟶ x6 x5) ⟶ x1.
Apply unknownprop_3bd96be69aa6ec3eecd6f9001283ba634547e4583192e2f0725cac970b330516 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Let x4 of type ι be given.
Assume H5: x4 ∈ x0.
Assume H6: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H7: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H8: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H9: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 : ι → ο . x6 x2 ⟶ x6 x3 ⟶ x6 x4 ⟶ x6 x5.
Apply or3E with
x2 ∈ x3,
x2 = x3,
x3 ∈ x2,
x1 leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
Assume H13: x2 ∈ x3.
Apply or3E with
x3 ∈ x4,
x3 = x4,
x4 ∈ x3,
x1 leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Assume H14: x3 ∈ x4.
Apply H2 with
x2,
x3,
x4 leaving 6 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H9.
Assume H14: x3 = x4.
Apply FalseE with
x1.
Apply H8.
The subproof is completed by applying H14.
Assume H14: x4 ∈ x3.
Apply or3E with
x2 ∈ x4,
x2 = x4,
x4 ∈ x2,
x1 leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x2,
x4 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L12.
Assume H15: x2 ∈ x4.
Apply H2 with
x2,
x4,
x3 leaving 6 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
The subproof is completed by applying H15.
The subproof is completed by applying H14.
Let x5 of type ι be given.
Assume H16: x5 ∈ x0.
Let x6 of type ι → ο be given.
Assume H17: x6 x2.
Assume H18: x6 x4.
Assume H19: x6 x3.
Apply H9 with
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
The subproof is completed by applying H19.
The subproof is completed by applying H18.
Assume H15: x2 = x4.
Apply FalseE with
x1.
Apply H7.
The subproof is completed by applying H15.
Assume H15: x4 ∈ x2.
Apply H2 with
x4,
x2,
x3 leaving 6 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H15.
The subproof is completed by applying H13.
Let x5 of type ι be given.
Assume H16: x5 ∈ x0.
Let x6 of type ι → ο be given.
Assume H17: x6 x4.
Assume H18: x6 x2.
Assume H19: x6 x3.
Apply H9 with
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H17.
Assume H13: x2 = x3.
Apply FalseE with
x1.
Apply H6.
The subproof is completed by applying H13.
Assume H13: x3 ∈ x2.
Apply or3E with
x3 ∈ x4,
x3 = x4,
x4 ∈ x3,
x1 leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Assume H14: x3 ∈ x4.
Apply or3E with
x2 ∈ x4,
x2 = x4,
x4 ∈ x2,
x1 leaving 4 subgoals.
Apply ordinal_trichotomy_or with
x2,
x4 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L12.
Assume H15: x2 ∈ x4.
Apply H2 with
x3,
x2,
x4 leaving 6 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Let x5 of type ι be given.
Assume H16: x5 ∈ x0.
Let x6 of type ι → ο be given.
Assume H17: x6 x3.
Assume H18: x6 x2.
Assume H19: x6 x4.
Apply H9 with
x5,
x6 leaving 4 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H18.
The subproof is completed by applying H17.
The subproof is completed by applying H19.
Assume H15: x2 = x4.
Apply FalseE with
x1.
Apply H7.
The subproof is completed by applying H15.