Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u10,
u6,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_40f47bd5727e3c8306e109a25c685ee358c3452e21455ab7ec4201d838abbfbf with
x0,
λ x2 . x0 = x2 ⟶ x1 x2 leaving 7 subgoals.
Apply setminusI with
u11,
u6,
x0 leaving 2 subgoals.
Apply ordsuccI1 with
u10,
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 u10.
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.