Prove there exists a surjective function from N to Z.
1 p ∈ F <-> ∃n ∈ N ∃z ∈ Z ^ p = ⟨n,z⟩ ^ φ(n,z)
2 F := {⟨x,y⟩:x∈N ^ y ∈ Z ^ φ(x,y)} \\shorthand for 1
3 φ(x,y) := ∃z∈N [(x=2z ^ y=z) v (x=2z+1 ^ y=-z)]
\\Prove F is a function:
4 N x Z = {x: n ∈ N ^ z ∈ Z ^ x = ⟨n, z⟩}
5 ∴F ⊆ N x Z \\from 2, since φ(n,z) is just a restriction on which n,z satisfy ⟨n,z⟩
6 ∴F ∈ P(N x Z)
7 If ⟨x',y_1⟩, ⟨x', y_2⟩ ∈ F:
8 φ(x, y_1) ^ φ(x, y_2)
9 z_1 := z_1 ∈ N ^ (x'=2z_1 ^ y_1=z_1) v (x'=2z_1 +1 ^ y_1=-z_1) \\from φ's definition
