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