Let x0 of type ι be given.
Apply setminusE with
omega,
Sing 0,
x0,
∀ x1 . nat_p x1 ⟶ 96eca.. x0 x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Claim L3: 0 ∈ x0
Apply nat_inv_impred with
λ x1 . nIn x1 (Sing 0) ⟶ 0 ∈ x1,
x0 leaving 4 subgoals.
Apply FalseE with
0 ∈ 0.
Apply H3.
The subproof is completed by applying SingI with 0.
Let x1 of type ι be given.
Apply nat_0_in_ordsucc with
x1.
The subproof is completed by applying H3.
Apply omega_nat_p with
x0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply nat_ind with
λ x1 . 96eca.. x0 x1 ∈ x0 leaving 2 subgoals.
Apply unknownprop_32031505644b872a0911c2de665524637f3e933b5a278f213bfb34b1b7b14a8c with
x0,
λ x1 x2 . x2 ∈ x0.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Apply xm with
ordsucc (96eca.. x0 x1) ∈ x0,
96eca.. x0 (ordsucc x1) ∈ x0 leaving 2 subgoals.
Apply unknownprop_0b6bf9289375e2fec7f133c86f85e21365e99b363c22a457be49ec227de43d5d with
x0,
x1,
λ x2 x3 . x3 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H6.
Apply unknownprop_5638b8a3f345573382122a22afd2c2865d379a7a354b4f08c0e6004c928d3e17 with
x0,
x1,
λ x2 x3 . x3 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying L3.