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