Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u14,
u10,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_148938b23ce1e09fe757ef9e6a301921596eef876225d13f1e17f527633e4cf2 with
x0,
λ x2 . x0 = x2 ⟶ x1 x2 leaving 7 subgoals.
Apply setminusI with
u15,
u10,
x0 leaving 2 subgoals.
Apply ordsuccI1 with
u14,
x0.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
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.
Apply FalseE with
x1 u14.
Apply In_irref with
x0.
Apply H7 with
λ x2 x3 . x0 ∈ x3.
The subproof is completed by applying H5.
Let x2 of type ι → ι → ο be given.
Assume H7: x2 x0 x0.
The subproof is completed by applying H7.