Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H1: x0 = 0 ⟶ x1.
Assume H2: x0 = 1 ⟶ x1.
Apply In_Power_ordsucc_cases_impred with
0,
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply H1.
Apply In_Power_0_eq_0 with
x0.
The subproof is completed by applying H3.
Assume H3: 0 ∈ x0.
Apply H2.
Apply set_ext with
x0,
1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H5: x2 ∈ x0.
Apply xm with
x2 ∈ Sing 0,
x2 ∈ 1 leaving 2 subgoals.
Apply SingE with
0,
x2,
λ x3 x4 . x4 ∈ 1 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying In_0_1.
Apply FalseE with
x2 ∈ 1.
Apply EmptyE with
x2.
Apply In_Power_0_eq_0 with
setminus x0 (Sing 0),
λ x3 x4 . x2 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply setminusI with
x0,
Sing 0,
x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Let x2 of type ι be given.
Assume H5: x2 ∈ 1.
Apply cases_1 with
x2,
λ x3 . x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.