Theorem nqereu 10685

Description: There is a unique element of Q equivalent to each element of N × N. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
nqereu	⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem nqereu

Dummy variables 𝑎 𝑏 𝑦 𝑐 𝑑 𝑚 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5613	. . 3 ⊢ (𝐴 ∈ (N × N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩)
2		pion 10635	. . . . . . . . 9 ⊢ (𝑏 ∈ N → 𝑏 ∈ On)
3		suceloni 7659	. . . . . . . . 9 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ N → suc 𝑏 ∈ On)
5		vex 3436	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6	5	sucid 6345	. . . . . . . 8 ⊢ 𝑏 ∈ suc 𝑏
7		eleq2 2827	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏))
8	7	rspcev 3561	. . . . . . . 8 ⊢ ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
9	4, 6, 8	sylancl 586	. . . . . . 7 ⊢ (𝑏 ∈ N → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
10	9	adantl 482	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
11		elequ2 2121	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚))
12	11	imbi1d 342	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
13	12	2ralbidv 3129	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
14		opeq1 4804	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
15	14	breq2d 5086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑑⟩))
16	15	rexbidv 3226	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩))
17	16	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩)))
18		elequ1 2113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
19		opeq2 4805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
20	19	breq2d 5086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
21	20	rexbidv 3226	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
22	18, 21	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
23	17, 22	cbvral2vw 3396	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
24	23	ralbii 3092	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
25		rexnal 3169	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏))
26		pm4.63 398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏))
27		xp2nd 7864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (N × N) → (2nd ‘𝑧) ∈ N)
28		ltpiord 10643	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
29	28	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ N ∧ (2nd ‘𝑧) ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
30	27, 29	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ N ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
31	30	adantll 711	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
32	31	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
33	26, 32	bitrid 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
34	33	rexbidva 3225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
35	25, 34	bitr3id 285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
36		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → (1st ‘𝑧) ∈ N)
37		elequ2 2121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏))
38	37	imbi1d 342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
39	38	2ralbidv 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
40	39	rspccv 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
41		opeq1 4804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 = (1st ‘𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st ‘𝑧), 𝑑⟩)
42	41	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
43	42	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
44	43	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
45	44	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
46	45	rspccv 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
47		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
48		opeq2 4805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 = (2nd ‘𝑧) → ⟨(1st ‘𝑧), 𝑑⟩ = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
49	48	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
50	49	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
51	47, 50	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑑 = (2nd ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) ↔ ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
52	51	rspccv 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
53	46, 52	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
54	40, 53	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))))
55	54	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
56	36, 55	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
57	27, 56	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
58	57	3imp 1110	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
59		1st2nd2 7870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
60	59	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
61	60	rexbidv 3226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (N × N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
62	61	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
63	58, 62	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧)
64		enqer 10677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ~Q Er (N × N)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ~Q Er (N × N))
66		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
68	65, 66, 67	ertr4d 8517	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q ⟨𝑎, 𝑏⟩)
69	68	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨𝑎, 𝑏⟩))
70	69	reximdv 3202	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
71	63, 70	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
72	71	3expia 1120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
73	72	impcomd 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
74	73	rexlimdva 3213	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
75	74	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
76	75	com3r 87	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
77	35, 76	syl6bi 252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
78	77	com13 88	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
79		mulcompi 10652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
80		enqbreq 10675	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑎 ∈ N ∧ 𝑏 ∈ N)) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
81	80	anidms 567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
82	79, 81	mpbiri 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩)
83		opelxpi 5626	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
84		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
85		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
86	85, 5	op2ndd 7842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
87	86	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N 𝑏))
88	87	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N 𝑏))
89	84, 88	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
90	89	ralbidv 3112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
91		df-nq 10668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))}
92	90, 91	elrab2 3627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
93	92	simplbi2 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ (N × N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
94	83, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
95		breq1 5077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩))
96	95	rspcev 3561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
97	96	expcom 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ → (⟨𝑎, 𝑏⟩ ∈ Q → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
98	82, 94, 97	sylsyld 61	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
99	98	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
100	99	a1dd 50	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
101	78, 100	pm2.61d2 181	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
102	101	ralrimivv 3122	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
103	24, 102	sylbir 234	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
104	103	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
105	13, 104	tfis2 7703	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
106		rsp 3131	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
108		rsp 3131	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
109	107, 108	syl6 35	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
110	109	impd 411	. . . . . . . 8 ⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
111	110	com12 32	. . . . . . 7 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑦 ∈ On → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
112	111	rexlimdv 3212	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
113	10, 112	mpd 15	. . . . 5 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
114		breq2 5078	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
115	114	rexbidv 3226	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
116	113, 115	syl5ibrcom 246	. . . 4 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴))
117	116	rexlimivv 3221	. . 3 ⊢ (∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
118	1, 117	sylbi 216	. 2 ⊢ (𝐴 ∈ (N × N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
119		breq2 5078	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴))
120		breq2 5078	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴))
121	119, 120	anbi12d 631	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴)))
122	121	imbi1d 342	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
123	122	2ralbidv 3129	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
124	64	a1i 11	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → ~Q Er (N × N))
125		simpl 483	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
126		simpr 485	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
127	124, 125, 126	ertr4d 8517	. . . . 5 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
128		mulcompi 10652	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
129		elpqn 10681	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Q → 𝑦 ∈ (N × N))
130		breq1 5077	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧))
131		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥))
132	131	breq2d 5086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N (2nd ‘𝑥)))
133	132	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
134	130, 133	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
135	134	ralbidv 3112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
136	135, 91	elrab2 3627	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
137	136	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
138		breq2 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦))
139		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦))
140	139	breq1d 5084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N (2nd ‘𝑥) ↔ (2nd ‘𝑦) <N (2nd ‘𝑥)))
141	140	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑥) ↔ ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
142	138, 141	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))))
143	142	rspcva 3559	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
144	129, 137, 143	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
145	144	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))
146		elpqn 10681	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
147	91	rabeq2i 3422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))))
148	147	simprbi 497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)))
149		breq2 5078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥))
150		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥))
151	150	breq1d 5084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑥) <N (2nd ‘𝑦)))
152	151	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
153	149, 152	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))))
154	153	rspcva 3559	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
155	146, 148, 154	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
156	64	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ~Q 𝑦 → ~Q Er (N × N))
157		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ~Q 𝑦 → 𝑥 ~Q 𝑦)
158	156, 157	ersym 8510	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥)
159	155, 158	impel 506	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))
160		xp2nd 7864	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
161	146, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
162	161	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) ∈ N)
163		xp2nd 7864	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (N × N) → (2nd ‘𝑦) ∈ N)
164	129, 163	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → (2nd ‘𝑦) ∈ N)
165	164	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑦) ∈ N)
166		ltsopi 10644	. . . . . . . . . . . . . . . . . . 19 ⊢ <N Or N
167		sotric 5531	. . . . . . . . . . . . . . . . . . 19 ⊢ (( <N Or N ∧ ((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
168	166, 167	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
169	168	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
170		notnotb 315	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
171	169, 170	bitr4di 289	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
172	162, 165, 171	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
173	159, 172	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
174	173	ord 861	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd ‘𝑦) <N (2nd ‘𝑥)))
175	145, 174	mt3d 148	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦))
176	175	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
177	128, 176	eqtrid 2790	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
178		1st2nd2 7870	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
179		1st2nd2 7870	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
180	178, 179	breqan12d 5090	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
181		xp1st 7863	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
182	181, 160	jca 512	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → ((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N))
183		xp1st 7863	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (N × N) → (1st ‘𝑦) ∈ N)
184	183, 163	jca 512	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N))
185		enqbreq 10675	. . . . . . . . . . . . . 14 ⊢ ((((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) ∧ ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
186	182, 184, 185	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
187	180, 186	bitrd 278	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
188	146, 129, 187	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
189	188	biimpa 477	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
190	177, 189	eqtrd 2778	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
191	146	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
192		mulcanpi 10656	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
193	160, 181, 192	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑥 ∈ (N × N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
194	191, 193	syl 17	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
195	190, 194	mpbid 231	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦))
196	195, 175	opeq12d 4812	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
197	191, 178	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
198	129	ad2antlr 724	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
199	198, 179	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
200	196, 197, 199	3eqtr4d 2788	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
201	200	ex 413	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → 𝑥 = 𝑦))
202	127, 201	syl5 34	. . . 4 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
203	202	rgen2 3120	. . 3 ⊢ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
204	123, 203	vtoclg 3505	. 2 ⊢ (𝐴 ∈ (N × N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
205		breq1 5077	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴))
206	205	reu4 3666	. 2 ⊢ (∃!𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
207	118, 204, 206	sylanbrc 583	1 ⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  ⟨cop 4567   class class class wbr 5074   Or wor 5502   × cxp 5587  Oncon0 6266  suc csuc 6268  ‘cfv 6433  (class class class)co 7275  1^st c1st 7829  2^nd c2nd 7830   Er wer 8495  Ncnpi 10600   ·_N cmi 10602   <_N clti 10603   ~_Q ceq 10607  Qcnq 10608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-oadd 8301  df-omul 8302  df-er 8498  df-ni 10628  df-mi 10630  df-lti 10631  df-enq 10667  df-nq 10668

This theorem is referenced by:  nqerf  10686  enqeq  10690