\\Header
PA1 ∀k∈N ∃m∈N ( k = m·2 ∨ k = m·2+1 )
PA1* ∀k,m ∈ N (k = 2m -> ¬∃n ∈ N (k = 2n+1)) \\modified PA1
P1 Z ∈ set
P2 φ is a property with two parameters and ∀x∀y: φ(x,y) <-> ∃z∈N [(x=2z ^ y=z) v (x=2z+1 ^ y=-z)]
P3 y ∈ {x : ψ(x)} <-> ψ(y)
P4 N ⊆ Z

\\Prove F := {⟨x,y⟩:x∈N ^ y ∈ Z ^ φ(x,y)} is a set in P(N x Z)
1 N x Z ∈ set \\from P1, **naturals**, **product-type**
2 F = {p: p ∈ N x Z ^ ∃n ∈ N ∃z ∈ Z (p = ⟨n,z⟩ ^ φ(n,z))} ∈ set \\from **comprehension**
3 p ∈ F <-> p ∈ N x Z \\from 3, P3
4 F ⊆ N x Z
5 F ∈ P(N x Z)

\\Prove ∀n ∈ N: ∃x ∈ F ∃z ∈ Z: x = ⟨n, z⟩
6 Given n ∈ N:
7	m := n = 2m ∨ n = 2m+1 \\from PA1
8	m ∈ Z \\from P4
9	If n = 2m:
10		∃z ∈ N (n = 2z ^ m = z)
11		φ(n, m) = ∃z∈N [(n=2z ^ m=z) v (n=2z+1 ^ m=-z)] = T
12		n ∈ N ^ m ∈ Z ^ ⟨n,m⟩ ∈ N x Z ^ φ(n,m)=T
13		⟨n,m⟩ ∈ F \\from P3 with 12 and 2
14		∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩
15	n = 2m -> ∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩

16	If n = 2m+1:
17		∃z ∈ N (n = 2z+1 ^ -m = -z)
18		φ(n, -m) = ∃z∈N [(n=2z ^ -m=z) v (n=2z+1 ^ -m=-z)] = T
19		n ∈ N ^ -m ∈ Z ^ ⟨n,m⟩ ∈ N x Z ^ φ(n,m)=T
20		⟨n,-m⟩ ∈ F
20		∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩
22	n = 2m+1 -> ∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩
23	n = 2m -> ∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩ \\restating 14
24	n = 2m ∨ n = 2m+1 \\restating 7
25	∃x ∈ F: ∃z ∈ Z: x = ⟨n, z⟩
26 ∀n ∈ N: ∃x ∈ F ∃z ∈ Z: x = ⟨n, z⟩

\\Prove ⟨x',y_1⟩, ⟨x', y_2⟩ ∈ F implies y_1 = y_2
27 If ⟨x',y_1⟩, ⟨x', y_2⟩ ∈ F:
28	φ(x', y_1) ^ φ(x', y_2) \\from 27, P2
29	z_1 := z_1 ∈ N ^ (x'=2z_1 ∧ y_1=z_1) ∨ (x'=2z_1 +1 ∧ y_1=-z_1)	\\from 28, P2
30	z_2 := z_2 ∈ N ^ (x'=2z_2 ∧ y_2=z_2) ∨ (x'=2z_2 +1 ∧ y_2=-z_2)	\\from 28, P2

31	If x' = 2z_1:
32		y_1 = z_1 \\from 29
33		x'=2z_2 ^ y_2=z_2 ∨ x' = 2z_2+1 ^ y_2=-z_2 \\from 30

34		If x'=2z_2:
35			x' = 2z_1 = 2z_2
36			z_1 = z_2
37			y_2 = z_1
38			y_1 = y_2
39		x'=2z_2 -> y_1 = y_2

40		If x'=2z_2+1:
41			2z_1 = 2z_2+1
42			⊥ (PA1*)
43		¬(x' = 2z_2 + 1)
44		x'=2z_2 \\disjunctive syllogism with 33
45		y_1 = y_2 \\from 39
46	x' = 2z_1 -> y_1 = y_2

47	If x' = 2z_1 + 1:
48		y_1 = -z_1 \\from 29
49		x'=2z_2 ^ y_2=z_2 ∨ x' = 2z_2+1 ^ y_2=-z_2 \\from 30

50		If x' = 2z_2 + 1:
51			2z_1 + 1 = 2z_2 + 1
52			z_1 = z_2
53			y_2 = -z_1
54		x' = 2z_2 + 1 -> y_1 = y_2

55		If x'=2z_2:
56			2z_2 = 2z_1 + 1
57			⊥ (PA1*)
58		x' = 2z_2 + 1 \\disjunctive syllogism
59		y_1 = y_2
60	x' = 2z_1 + 1 -> y_1 = y_2
61
62	x' = 2z_1 -> y_1 = y_2 \\restating 46
63	x' = 2z_1 + 1 -> y_1 = y_2 \restating 60
64	x' = 2z_1 ∨ x' = 2z_1 + 1 \\from 29
65	y_1 = y_2
66 ⟨x',y_1⟩, ⟨x', y_2⟩ ∈ F -> y_1 = y_2

67 ∀n ∈ N: ∃x ∈ F ∃z ∈ Z: x = ⟨n, z⟩ \\restating 26
68 F ∈ P(N x Z) \\restating 5

69 ∴F satisfies **function-type** \\from 66,67,68