Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: finite {x0 ∈ omega|prime_nat x0}.
Apply H0 with False.
Let x0 of type ι be given.
Assume H1: (λ x1 . and (x1 ∈ omega) (equip {x2 ∈ omega|prime_nat x2} x1)) x0.
Apply H1 with False.
Assume H2: x0 ∈ omega.
Assume H3: equip {x1 ∈ omega|prime_nat x1} x0.
Claim L4: equip x0 {x1 ∈ omega|prime_nat x1}
Apply equip_sym with {x1 ∈ omega|prime_nat x1}, x0.
The subproof is completed by applying H3.
Apply L4 with False.
Let x1 of type ι → ι be given.
Assume H5: bij x0 {x2 ∈ omega|prime_nat x2} x1.
Claim L6: surj x0 {x2 ∈ omega|prime_nat x2} x1
Apply bij_surj with x0, {x2 ∈ omega|prime_nat x2}, x1.
The subproof is completed by applying H5.
Apply unknownprop_8f5b0d62af687a637762403d82fd2db1c120b30f5359bb1eb2c486817c849925 with x0, x1 leaving 2 subgoals.
Apply omega_nat_p with x0.
The subproof is completed by applying H2.
The subproof is completed by applying L6.
■