Theorem nqereu 10902

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 5676	. . 3 ⊢ (𝐴 ∈ (N × N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩)
2		pion 10852	. . . . . . . . 9 ⊢ (𝑏 ∈ N → 𝑏 ∈ On)
3		onsuc 7797	. . . . . . . . 9 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
4	2, 3	syl 18	. . . . . . . 8 ⊢ (𝑏 ∈ N → suc 𝑏 ∈ On)
5		vex 3461	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6	5	sucid 6434	. . . . . . . 8 ⊢ 𝑏 ∈ suc 𝑏
7		eleq2 2854	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏))
8	7	rspcev 3584	. . . . . . . 8 ⊢ ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
9	4, 6, 8	sylancl 597	. . . . . . 7 ⊢ (𝑏 ∈ N → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
10	9	adantl 486	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
11		elequ2 2160	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚))
12	11	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
13	12	2ralbidv 3229	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
14		opeq1 4834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
15	14	breq2d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑑⟩))
16	15	rexbidv 3189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩))
17	16	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩)))
18		elequ1 2152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
19		opeq2 4835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
20	19	breq2d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
21	20	rexbidv 3189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
22	18, 21	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
23	17, 22	cbvral2vw 3247	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
24	23	ralbii 3111	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
25		rexnal 3117	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏))
26		pm4.63 402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏))
27		xp2nd 8007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (N × N) → (2nd ‘𝑧) ∈ N)
28		ltpiord 10860	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
29	28	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ N ∧ (2nd ‘𝑧) ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
30	27, 29	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ N ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
31	30	adantll 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
32	31	anbi2d 641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
33	26, 32	bitrid 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
34	33	rexbidva 3187	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
35	25, 34	bitr3id 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
36		xp1st 8006	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → (1st ‘𝑧) ∈ N)
37		elequ2 2160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏))
38	37	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
39	38	2ralbidv 3229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
40	39	rspccv 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
41		opeq1 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 = (1st ‘𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st ‘𝑧), 𝑑⟩)
42	41	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
43	42	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
44	43	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
45	44	ralbidv 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
46	45	rspccv 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
47		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
48		opeq2 4835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 = (2nd ‘𝑧) → ⟨(1st ‘𝑧), 𝑑⟩ = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
49	48	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
50	49	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
53	46, 52	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
54	40, 53	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))))
55	54	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
56	36, 55	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
57	27, 56	mpdi 46	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
58	57	3imp 1126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
59		1st2nd2 8013	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
60	59	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
61	60	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (N × N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
62	61	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
63	58, 62	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧)
64		enqer 10894	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ~Q Er (N × N)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ~Q Er (N × N))
66		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
68	65, 66, 67	ertr4d 8702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q ⟨𝑎, 𝑏⟩)
69	68	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨𝑎, 𝑏⟩))
70	69	reximdv 3180	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
71	63, 70	syl5com 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
72	71	3expia 1137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
73	72	impcomd 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
74	73	rexlimdva 3166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
75	74	ex 417	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
76	75	com3r 88	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
77	35, 76	biimtrdi 256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
78	77	com13 89	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
79		mulcompi 10869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
80		enqbreq 10892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑎 ∈ N ∧ 𝑏 ∈ N)) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
81	80	anidms 576	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
82	79, 81	mpbiri 261	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩)
83		opelxpi 5689	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
84		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
85		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
86	85, 5	op2ndd 7985	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
87	86	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N 𝑏))
88	87	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N 𝑏))
89	84, 88	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
90	89	ralbidv 3188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
91		df-nq 10885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))}
92	90, 91	elrab2 3657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
93	92	simplbi2 505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ (N × N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
94	83, 93	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
95		breq1 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩))
96	95	rspcev 3584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
97	96	expcom 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ → (⟨𝑎, 𝑏⟩ ∈ Q → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
98	82, 94, 97	sylsyld 62	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
99	98	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
100	99	a1dd 51	. . . . . . . . . . . . . . . 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 3206	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
103	24, 102	sylbir 238	. . . . . . . . . . . . 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 7841	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
106		rsp 3253	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
107	105, 106	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
108		rsp 3253	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
109	107, 108	syl6 36	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
110	109	impd 415	. . . . . . . 8 ⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
111	110	com12 33	. . . . . . 7 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑦 ∈ On → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
112	111	rexlimdv 3164	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
113	10, 112	mpd 16	. . . . 5 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
114		breq2 5109	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
115	114	rexbidv 3189	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
116	113, 115	syl5ibrcom 250	. . . 4 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴))
117	116	rexlimivv 3207	. . 3 ⊢ (∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
118	1, 117	sylbi 220	. 2 ⊢ (𝐴 ∈ (N × N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
119		breq2 5109	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴))
120		breq2 5109	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴))
121	119, 120	anbi12d 643	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴)))
122	121	imbi1d 344	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
123	122	2ralbidv 3229	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
124	64	a1i 11	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → ~Q Er (N × N))
125		simpl 487	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
126		simpr 489	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
127	124, 125, 126	ertr4d 8702	. . . . 5 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
128		mulcompi 10869	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
129		elpqn 10898	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Q → 𝑦 ∈ (N × N))
130		breq1 5108	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧))
131		fveq2 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥))
132	131	breq2d 5117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N (2nd ‘𝑥)))
133	132	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
134	130, 133	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
135	134	ralbidv 3188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
136	135, 91	elrab2 3657	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
137	136	simprbi 502	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
138		breq2 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦))
139		fveq2 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦))
140	139	breq1d 5115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N (2nd ‘𝑥) ↔ (2nd ‘𝑦) <N (2nd ‘𝑥)))
141	140	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑥) ↔ ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
142	138, 141	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))))
143	142	rspcva 3582	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
144	129, 137, 143	syl2anr 608	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
145	144	imp 411	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))
146		elpqn 10898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
147	91	reqabi 3440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))))
148	147	simprbi 502	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)))
149		breq2 5109	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥))
150		fveq2 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥))
151	150	breq1d 5115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑥) <N (2nd ‘𝑦)))
152	151	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
153	149, 152	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))))
154	153	rspcva 3582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
155	146, 148, 154	syl2an 607	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
156	64	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ~Q 𝑦 → ~Q Er (N × N))
157		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ~Q 𝑦 → 𝑥 ~Q 𝑦)
158	156, 157	ersym 8695	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥)
159	155, 158	impel 514	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))
160		xp2nd 8007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
161	146, 160	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
162	161	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) ∈ N)
163		xp2nd 8007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (N × N) → (2nd ‘𝑦) ∈ N)
164	129, 163	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → (2nd ‘𝑦) ∈ N)
165	164	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑦) ∈ N)
166		ltsopi 10861	. . . . . . . . . . . . . . . . . . 19 ⊢ <N Or N
167		sotric 5590	. . . . . . . . . . . . . . . . . . 19 ⊢ (( <N Or N ∧ ((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
168	166, 167	mpan 702	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
169	168	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
170		notnotb 318	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
171	169, 170	bitr4di 292	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
172	162, 165, 171	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
173	159, 172	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
174	173	ord 877	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd ‘𝑦) <N (2nd ‘𝑥)))
175	145, 174	mt3d 149	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦))
176	175	oveq2d 7416	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
177	128, 176	eqtrid 2812	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
178		1st2nd2 8013	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
179		1st2nd2 8013	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
180	178, 179	breqan12d 5121	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
181		xp1st 8006	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
182	181, 160	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → ((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N))
183		xp1st 8006	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (N × N) → (1st ‘𝑦) ∈ N)
184	183, 163	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N))
185		enqbreq 10892	. . . . . . . . . . . . . 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 607	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
187	180, 186	bitrd 282	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
188	146, 129, 187	syl2an 607	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
189	188	biimpa 481	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
190	177, 189	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
191	146	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
192		mulcanpi 10873	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
193	160, 181, 192	syl2anc 595	. . . . . . . . . 10 ⊢ (𝑥 ∈ (N × N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
194	191, 193	syl 18	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
195	190, 194	mpbid 235	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦))
196	195, 175	opeq12d 4842	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
197	191, 178	syl 18	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
198	129	ad2antlr 739	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
199	198, 179	syl 18	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
200	196, 197, 199	3eqtr4d 2810	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
201	200	ex 417	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → 𝑥 = 𝑦))
202	127, 201	syl5 35	. . . 4 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
203	202	rgen2 3205	. . 3 ⊢ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
204	123, 203	vtoclg 3525	. 2 ⊢ (𝐴 ∈ (N × N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
205		breq1 5108	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴))
206	205	reu4 3697	. 2 ⊢ (∃!𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
207	118, 204, 206	sylanbrc 594	1 ⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089  ∃!wreu 3368  ⟨cop 4591   class class class wbr 5105   Or wor 5559   × cxp 5650  Oncon0 6350  suc csuc 6352  ‘cfv 6525  (class class class)co 7400  1^st c1st 7972  2^nd c2nd 7973   Er wer 8679  Ncnpi 10817   ·_N cmi 10819   <_N clti 10820   ~_Q ceq 10824  Qcnq 10825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-oadd 8445  df-omul 8446  df-er 8682  df-ni 10845  df-mi 10847  df-lti 10848  df-enq 10884  df-nq 10885

This theorem is referenced by:  nqerf  10903  enqeq  10907