Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 = 0 ⟶ ∀ x2 : ο . x2.
Apply H1 with
or (x0 ∈ x1) (x0 = x1).
Apply H2 with
(∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1)) ⟶ or (x0 ∈ x1) (x0 = x1).
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
Apply nat_p_ordinal with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H4.
Apply ordinal_In_Or_Subq with
x0,
x1,
or (x0 ∈ x1) (x0 = x1) leaving 4 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Assume H8: x0 ∈ x1.
Apply orIL with
x0 ∈ x1,
x0 = x1.
The subproof is completed by applying H8.
Assume H8: x1 ⊆ x0.
Apply orIR with
x0 ∈ x1,
x0 = x1.
Apply set_ext with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_9ad0867fc87b914742fe6e9dd13399a9059e30111d97034a5ca39a2e1dce3530 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H8.