Let x0 of type ο be given.
Apply H0 with
λ x1 . PSNo omega (λ x2 . or (x2 ∈ {mul_nat 2 x3|x3 ∈ x1}) (x2 ∈ {ordsucc (mul_nat 2 x3)|x3 ∈ omega,nIn x3 x1})).
Apply andI with
∀ x1 . x1 ∈ prim4 omega ⟶ (λ x2 . PSNo omega (λ x3 . or (x3 ∈ {mul_nat 2 x4|x4 ∈ x2}) (x3 ∈ {ordsucc (mul_nat 2 x4)|x4 ∈ omega,nIn x4 x2}))) x1 ∈ real,
∀ x1 . x1 ∈ prim4 omega ⟶ ∀ x2 . x2 ∈ prim4 omega ⟶ (λ x3 . PSNo omega (λ x4 . or (x4 ∈ {mul_nat 2 x5|x5 ∈ x3}) (x4 ∈ {ordsucc (mul_nat 2 x5)|x5 ∈ omega,nIn x5 x3}))) x1 = (λ x3 . PSNo omega (λ x4 . or (x4 ∈ {mul_nat 2 x5|x5 ∈ x3}) (x4 ∈ {ordsucc (mul_nat 2 x5)|x5 ∈ omega,nIn x5 x3}))) x2 ⟶ x1 = x2 leaving 2 subgoals.
Let x1 of type ι be given.
Apply real_I with
(λ x2 . PSNo omega (λ x3 . or (x3 ∈ {mul_nat 2 x4|x4 ∈ x2}) (x3 ∈ {ordsucc (mul_nat 2 x4)|x4 ∈ omega,nIn x4 x2}))) x1 leaving 4 subgoals.
Apply SNoS_I with
ordsucc omega,
(λ x2 . PSNo omega (λ x3 . or (x3 ∈ {mul_nat 2 x4|x4 ∈ x2}) (x3 ∈ {ordsucc (mul_nat 2 x4)|x4 ∈ omega,nIn x4 x2}))) x1,
omega leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying ordsuccI2 with
omega.
The subproof is completed by applying L7.
Assume H11: 0 ∈ x1.
Apply L3 with
x1,
0 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H11.
Apply H10 with
λ x2 x3 . ordsucc (mul_nat 2 0) ∈ x3.
Apply omega_ordsucc with
mul_nat 2 0.
Apply mul_nat_0R with
2,
λ x2 x3 . x3 ∈ omega.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply L11.
Apply L2 with
x1,
0 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply H10 with
λ x2 x3 . mul_nat 2 0 ∈ x3.
Apply mul_nat_0R with
2,
λ x2 x3 . x3 ∈ omega.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.