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