Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 = 0 ⟶ ∀ x2 : ο . x2.
Apply H1 with
x0 ⊆ x1.
Apply H2 with
(∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1)) ⟶ x0 ⊆ x1.
Assume H3:
x0 ∈ omega.
Assume H4:
x1 ∈ omega.
Apply H5 with
x0 ⊆ x1.
Let x2 of type ι be given.
Apply H6 with
x0 ⊆ x1.
Assume H7:
x2 ∈ omega.
Apply H8 with
λ x3 x4 . x0 ⊆ x3.
Apply unknownprop_0dc8d11d1ba28645d1565e6f95fe26f514da291413e114d0327c09556f7d23e9 with
x0,
x2 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
Apply setminusI with
omega,
1,
x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H9: x2 ∈ 1.
Apply H0.
Apply H8 with
λ x3 x4 . x3 = 0.
Apply cases_1 with
x2,
λ x3 . mul_nat x0 x3 = 0 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying mul_nat_0R with x0.