Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u15,
u10,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_f1726a1d650e197e8b9e627d68e9fc72305df4fc0fdc395e8e3ea52e95296f3d with
x0,
λ x2 . x0 = x2 ⟶ x1 x2 leaving 8 subgoals.
Apply setminusI with
u16,
u10,
x0 leaving 2 subgoals.
Apply ordsuccI1 with
u15,
x0.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply FalseE with
x1 u15.
Apply In_irref with
x0.
Apply H8 with
λ x2 x3 . x0 ∈ x3.
The subproof is completed by applying H6.
Let x2 of type ι → ι → ο be given.
Assume H8: x2 x0 x0.
The subproof is completed by applying H8.