Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply H1 with
False.
Assume H3:
∀ x2 . x2 ∈ {x3 ∈ omega|prime_nat x3} ⟶ ∃ x3 . and (x3 ∈ x0) (x1 x3 = x2).
Apply H3 with
ordsucc (nat_primrec 1 (λ x2 x3 . mul_nat (x1 x2) x3) x0),
False leaving 2 subgoals.
The subproof is completed by applying L9.
Let x2 of type ι be given.
Apply H10 with
False.
Assume H11: x2 ∈ x0.
Apply In_irref with
ordsucc (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0).
Apply H12 with
λ x3 x4 . x3 ∈ ordsucc (nat_primrec 1 (λ x5 x6 . mul_nat (x1 x5) x6) x0).
Apply SepE with
omega,
prime_nat,
x1 x2,
x1 x2 ∈ ordsucc (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0) leaving 2 subgoals.
Apply H2 with
x2.
The subproof is completed by applying H11.
Assume H13:
x1 x2 ∈ omega.
Apply ordinal_In_Or_Subq with
x1 x2,
ordsucc (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0),
x1 x2 ∈ ordsucc (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0) leaving 4 subgoals.
Apply nat_p_ordinal with
x1 x2.
Apply omega_nat_p with
x1 x2.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Apply FalseE with
x1 x2 ∈ ordsucc (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0).
Apply unknownprop_c9098cd36bcaebd859dfd7185424450a09bf20e6004a31ad115c63167c80e96f with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L6.
The subproof is completed by applying H11.