Theorem nqereu 10351

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 5579	. . 3 ⊢ (𝐴 ∈ (N × N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩)
2		pion 10301	. . . . . . . . 9 ⊢ (𝑏 ∈ N → 𝑏 ∈ On)
3		suceloni 7528	. . . . . . . . 9 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ N → suc 𝑏 ∈ On)
5		vex 3497	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6	5	sucid 6270	. . . . . . . 8 ⊢ 𝑏 ∈ suc 𝑏
7		eleq2 2901	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏))
8	7	rspcev 3623	. . . . . . . 8 ⊢ ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
9	4, 6, 8	sylancl 588	. . . . . . 7 ⊢ (𝑏 ∈ N → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
10	9	adantl 484	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
11		elequ2 2129	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚))
12	11	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
13	12	2ralbidv 3199	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
14		opeq1 4803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
15	14	breq2d 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑑⟩))
16	15	rexbidv 3297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩))
17	16	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩)))
18		elequ1 2121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
19		opeq2 4804	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
20	19	breq2d 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
21	20	rexbidv 3297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
22	18, 21	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
23	17, 22	cbvral2vw 3461	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
24	23	ralbii 3165	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
25		rexnal 3238	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏))
26		pm4.63 400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏))
27		xp2nd 7722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (N × N) → (2nd ‘𝑧) ∈ N)
28		ltpiord 10309	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
29	28	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ N ∧ (2nd ‘𝑧) ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
30	27, 29	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ N ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
31	30	adantll 712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
32	31	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
33	26, 32	syl5bb 285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
34	33	rexbidva 3296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
35	25, 34	syl5bbr 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
36		xp1st 7721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → (1st ‘𝑧) ∈ N)
37		elequ2 2129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏))
38	37	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
39	38	2ralbidv 3199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
40	39	rspccv 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
41		opeq1 4803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 = (1st ‘𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st ‘𝑧), 𝑑⟩)
42	41	breq2d 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
43	42	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
44	43	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
45	44	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
46	45	rspccv 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
47		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
48		opeq2 4804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 = (2nd ‘𝑧) → ⟨(1st ‘𝑧), 𝑑⟩ = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
49	48	breq2d 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
50	49	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
51	47, 50	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑑 = (2nd ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) ↔ ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
52	51	rspccv 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
59		1st2nd2 7728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
60	59	breq2d 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
61	60	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (N × N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
62	61	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
63	58, 62	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧)
64		enqer 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ~Q Er (N × N)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ~Q Er (N × N))
66		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
68	65, 66, 67	ertr4d 8308	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q ⟨𝑎, 𝑏⟩)
69	68	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨𝑎, 𝑏⟩))
70	69	reximdv 3273	. . . . . . . . . . . . . . . . . . . . . . . 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 1117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
73	72	impcomd 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
74	73	rexlimdva 3284	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
75	74	ex 415	. . . . . . . . . . . . . . . . . . 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 255	. . . . . . . . . . . . . . . . 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 10318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
80		enqbreq 10341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑎 ∈ N ∧ 𝑏 ∈ N)) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
81	80	anidms 569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
82	79, 81	mpbiri 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩)
83		opelxpi 5592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
84		breq1 5069	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
85		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
86	85, 5	op2ndd 7700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
87	86	breq2d 5078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N 𝑏))
88	87	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N 𝑏))
89	84, 88	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
90	89	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
91		df-nq 10334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))}
92	90, 91	elrab2 3683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
93	92	simplbi2 503	. . . . . . . . . . . . . . . . . . . 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 5069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩))
96	95	rspcev 3623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
97	96	expcom 416	. . . . . . . . . . . . . . . . . . 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 183	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
102	101	ralrimivv 3190	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
103	24, 102	sylbir 237	. . . . . . . . . . . . 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 7571	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
106		rsp 3205	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
108		rsp 3205	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
109	107, 108	syl6 35	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
110	109	impd 413	. . . . . . . 8 ⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
111	110	com12 32	. . . . . . 7 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑦 ∈ On → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
112	111	rexlimdv 3283	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
113	10, 112	mpd 15	. . . . 5 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
114		breq2 5070	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
115	114	rexbidv 3297	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
116	113, 115	syl5ibrcom 249	. . . 4 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴))
117	116	rexlimivv 3292	. . 3 ⊢ (∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
118	1, 117	sylbi 219	. 2 ⊢ (𝐴 ∈ (N × N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
119		breq2 5070	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴))
120		breq2 5070	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴))
121	119, 120	anbi12d 632	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴)))
122	121	imbi1d 344	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
123	122	2ralbidv 3199	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
124	64	a1i 11	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → ~Q Er (N × N))
125		simpl 485	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
126		simpr 487	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
127	124, 125, 126	ertr4d 8308	. . . . 5 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
128		mulcompi 10318	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
129		elpqn 10347	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Q → 𝑦 ∈ (N × N))
130		breq1 5069	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧))
131		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥))
132	131	breq2d 5078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N (2nd ‘𝑥)))
133	132	notbid 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
134	130, 133	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
135	134	ralbidv 3197	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
136	135, 91	elrab2 3683	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
137	136	simprbi 499	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
138		breq2 5070	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦))
139		fveq2 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦))
140	139	breq1d 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N (2nd ‘𝑥) ↔ (2nd ‘𝑦) <N (2nd ‘𝑥)))
141	140	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑥) ↔ ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
142	138, 141	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))))
143	142	rspcva 3621	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
144	129, 137, 143	syl2anr 598	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
145	144	imp 409	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))
146		elpqn 10347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
147	91	rabeq2i 3487	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))))
148	147	simprbi 499	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)))
149		breq2 5070	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥))
150		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥))
151	150	breq1d 5076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑥) <N (2nd ‘𝑦)))
152	151	notbid 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
153	149, 152	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))))
154	153	rspcva 3621	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
155	146, 148, 154	syl2an 597	. . . . . . . . . . . . . . . 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 8301	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥)
159	155, 158	impel 508	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))
160		xp2nd 7722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
161	146, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
162	161	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) ∈ N)
163		xp2nd 7722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (N × N) → (2nd ‘𝑦) ∈ N)
164	129, 163	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → (2nd ‘𝑦) ∈ N)
165	164	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑦) ∈ N)
166		ltsopi 10310	. . . . . . . . . . . . . . . . . . 19 ⊢ <N Or N
167		sotric 5501	. . . . . . . . . . . . . . . . . . 19 ⊢ (( <N Or N ∧ ((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
168	166, 167	mpan 688	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
169	168	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
170		notnotb 317	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
171	169, 170	syl6bbr 291	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
172	162, 165, 171	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
173	159, 172	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
174	173	ord 860	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd ‘𝑦) <N (2nd ‘𝑥)))
175	145, 174	mt3d 150	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦))
176	175	oveq2d 7172	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
177	128, 176	syl5eq 2868	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
178		1st2nd2 7728	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
179		1st2nd2 7728	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
180	178, 179	breqan12d 5082	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
181		xp1st 7721	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
182	181, 160	jca 514	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → ((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N))
183		xp1st 7721	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (N × N) → (1st ‘𝑦) ∈ N)
184	183, 163	jca 514	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N))
185		enqbreq 10341	. . . . . . . . . . . . . 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 597	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
187	180, 186	bitrd 281	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
188	146, 129, 187	syl2an 597	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
189	188	biimpa 479	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
190	177, 189	eqtrd 2856	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
191	146	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
192		mulcanpi 10322	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
193	160, 181, 192	syl2anc 586	. . . . . . . . . 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 234	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦))
196	195, 175	opeq12d 4811	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
197	191, 178	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
198	129	ad2antlr 725	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
199	198, 179	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
200	196, 197, 199	3eqtr4d 2866	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
201	200	ex 415	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → 𝑥 = 𝑦))
202	127, 201	syl5 34	. . . 4 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
203	202	rgen2 3203	. . 3 ⊢ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
204	123, 203	vtoclg 3567	. 2 ⊢ (𝐴 ∈ (N × N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
205		breq1 5069	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴))
206	205	reu4 3722	. 2 ⊢ (∃!𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
207	118, 204, 206	sylanbrc 585	1 ⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  ⟨cop 4573   class class class wbr 5066   Or wor 5473   × cxp 5553  Oncon0 6191  suc csuc 6193  ‘cfv 6355  (class class class)co 7156  1^st c1st 7687  2^nd c2nd 7688   Er wer 8286  Ncnpi 10266   ·_N cmi 10268   <_N clti 10269   ~_Q ceq 10273  Qcnq 10274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-oadd 8106  df-omul 8107  df-er 8289  df-ni 10294  df-mi 10296  df-lti 10297  df-enq 10333  df-nq 10334

This theorem is referenced by:  nqerf  10352  enqeq  10356