Theorem nqereu 10141

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 5424	. . 3 ⊢ (𝐴 ∈ (N × N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩)
2		pion 10091	. . . . . . . . 9 ⊢ (𝑏 ∈ N → 𝑏 ∈ On)
3		suceloni 7338	. . . . . . . . 9 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ N → suc 𝑏 ∈ On)
5		vex 3412	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6	5	sucid 6102	. . . . . . . 8 ⊢ 𝑏 ∈ suc 𝑏
7		eleq2 2848	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏))
8	7	rspcev 3529	. . . . . . . 8 ⊢ ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
9	4, 6, 8	sylancl 577	. . . . . . 7 ⊢ (𝑏 ∈ N → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
10	9	adantl 474	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
11		elequ2 2062	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚))
12	11	imbi1d 334	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
13	12	2ralbidv 3143	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
14		opeq1 4671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
15	14	breq2d 4935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑑⟩))
16	15	rexbidv 3236	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩))
17	16	imbi2d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩)))
18		elequ1 2055	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
19		opeq2 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
20	19	breq2d 4935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
21	20	rexbidv 3236	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
22	18, 21	imbi12d 337	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
23	17, 22	cbvral2v 3386	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
24	23	ralbii 3109	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
25		rexnal 3179	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏))
26		pm4.63 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏))
27		xp2nd 7527	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (N × N) → (2nd ‘𝑧) ∈ N)
28		ltpiord 10099	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
29	28	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ N ∧ (2nd ‘𝑧) ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
30	27, 29	sylan2 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ N ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
31	30	adantll 701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
32	31	anbi2d 619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
33	26, 32	syl5bb 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
34	33	rexbidva 3235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
35	25, 34	syl5bbr 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
36		xp1st 7526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → (1st ‘𝑧) ∈ N)
37		elequ2 2062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏))
38	37	imbi1d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
39	38	2ralbidv 3143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
40	39	rspccv 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
41		opeq1 4671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 = (1st ‘𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st ‘𝑧), 𝑑⟩)
42	41	breq2d 4935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
43	42	rexbidv 3236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
44	43	imbi2d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
45	44	ralbidv 3141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
46	45	rspccv 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
47		eleq1 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
48		opeq2 4672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 = (2nd ‘𝑧) → ⟨(1st ‘𝑧), 𝑑⟩ = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
49	48	breq2d 4935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
50	49	rexbidv 3236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
51	47, 50	imbi12d 337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑑 = (2nd ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) ↔ ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
52	51	rspccv 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1091	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
59		1st2nd2 7533	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
60	59	breq2d 4935	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
61	60	rexbidv 3236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (N × N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
62	61	3ad2ant2 1114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
63	58, 62	mpbird 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧)
64		enqer 10133	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ~Q Er (N × N)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ~Q Er (N × N))
66		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67		simpl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
68	65, 66, 67	ertr4d 8100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q ⟨𝑎, 𝑏⟩)
69	68	ex 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨𝑎, 𝑏⟩))
70	69	reximdv 3212	. . . . . . . . . . . . . . . . . . . . . . . 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 1101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
73	72	impcomd 403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
74	73	rexlimdva 3223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
75	74	ex 405	. . . . . . . . . . . . . . . . . . 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 245	. . . . . . . . . . . . . . . . 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 10108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
80		enqbreq 10131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑎 ∈ N ∧ 𝑏 ∈ N)) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
81	80	anidms 559	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
82	79, 81	mpbiri 250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩)
83		opelxpi 5437	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
84		breq1 4926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
85		vex 3412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
86	85, 5	op2ndd 7505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
87	86	breq2d 4935	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N 𝑏))
88	87	notbid 310	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N 𝑏))
89	84, 88	imbi12d 337	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
90	89	ralbidv 3141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
91		df-nq 10124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))}
92	90, 91	elrab2 3593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
93	92	simplbi2 493	. . . . . . . . . . . . . . . . . . . 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 4926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩))
96	95	rspcev 3529	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
97	96	expcom 406	. . . . . . . . . . . . . . . . . . 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 174	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
102	101	ralrimivv 3134	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
103	24, 102	sylbir 227	. . . . . . . . . . . . 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 7381	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
106		rsp 3149	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
108		rsp 3149	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
109	107, 108	syl6 35	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
110	109	impd 402	. . . . . . . 8 ⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
111	110	com12 32	. . . . . . 7 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑦 ∈ On → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
112	111	rexlimdv 3222	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
113	10, 112	mpd 15	. . . . 5 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
114		breq2 4927	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
115	114	rexbidv 3236	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
116	113, 115	syl5ibrcom 239	. . . 4 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴))
117	116	rexlimivv 3231	. . 3 ⊢ (∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
118	1, 117	sylbi 209	. 2 ⊢ (𝐴 ∈ (N × N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
119		breq2 4927	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴))
120		breq2 4927	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴))
121	119, 120	anbi12d 621	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴)))
122	121	imbi1d 334	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
123	122	2ralbidv 3143	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
124	64	a1i 11	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → ~Q Er (N × N))
125		simpl 475	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
126		simpr 477	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
127	124, 125, 126	ertr4d 8100	. . . . 5 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
128		mulcompi 10108	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
129		elpqn 10137	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Q → 𝑦 ∈ (N × N))
130		breq1 4926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧))
131		fveq2 6493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥))
132	131	breq2d 4935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N (2nd ‘𝑥)))
133	132	notbid 310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
134	130, 133	imbi12d 337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
135	134	ralbidv 3141	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
136	135, 91	elrab2 3593	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
137	136	simprbi 489	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
138		breq2 4927	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦))
139		fveq2 6493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦))
140	139	breq1d 4933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N (2nd ‘𝑥) ↔ (2nd ‘𝑦) <N (2nd ‘𝑥)))
141	140	notbid 310	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑥) ↔ ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
142	138, 141	imbi12d 337	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))))
143	142	rspcva 3527	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
144	129, 137, 143	syl2anr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
145	144	imp 398	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))
146		elpqn 10137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
147	91	rabeq2i 3404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))))
148	147	simprbi 489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)))
149		breq2 4927	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥))
150		fveq2 6493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥))
151	150	breq1d 4933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑥) <N (2nd ‘𝑦)))
152	151	notbid 310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
153	149, 152	imbi12d 337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))))
154	153	rspcva 3527	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
155	146, 148, 154	syl2an 586	. . . . . . . . . . . . . . . 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 8093	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥)
159	155, 158	impel 498	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))
160		xp2nd 7527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
161	146, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
162	161	ad2antrr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) ∈ N)
163		xp2nd 7527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (N × N) → (2nd ‘𝑦) ∈ N)
164	129, 163	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → (2nd ‘𝑦) ∈ N)
165	164	ad2antlr 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑦) ∈ N)
166		ltsopi 10100	. . . . . . . . . . . . . . . . . . 19 ⊢ <N Or N
167		sotric 5346	. . . . . . . . . . . . . . . . . . 19 ⊢ (( <N Or N ∧ ((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
168	166, 167	mpan 677	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
169	168	notbid 310	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
170		notnotb 307	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
171	169, 170	syl6bbr 281	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
172	162, 165, 171	syl2anc 576	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
173	159, 172	mpbid 224	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
174	173	ord 850	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd ‘𝑦) <N (2nd ‘𝑥)))
175	145, 174	mt3d 143	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦))
176	175	oveq2d 6986	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
177	128, 176	syl5eq 2820	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
178		1st2nd2 7533	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
179		1st2nd2 7533	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
180	178, 179	breqan12d 4939	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
181		xp1st 7526	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
182	181, 160	jca 504	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → ((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N))
183		xp1st 7526	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (N × N) → (1st ‘𝑦) ∈ N)
184	183, 163	jca 504	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N))
185		enqbreq 10131	. . . . . . . . . . . . . 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 586	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
187	180, 186	bitrd 271	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
188	146, 129, 187	syl2an 586	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
189	188	biimpa 469	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
190	177, 189	eqtrd 2808	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
191	146	ad2antrr 713	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
192		mulcanpi 10112	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
193	160, 181, 192	syl2anc 576	. . . . . . . . . 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 224	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦))
196	195, 175	opeq12d 4679	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
197	191, 178	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
198	129	ad2antlr 714	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
199	198, 179	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
200	196, 197, 199	3eqtr4d 2818	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
201	200	ex 405	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → 𝑥 = 𝑦))
202	127, 201	syl5 34	. . . 4 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
203	202	rgen2a 3170	. . 3 ⊢ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
204	123, 203	vtoclg 3480	. 2 ⊢ (𝐴 ∈ (N × N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
205		breq1 4926	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴))
206	205	reu4 3630	. 2 ⊢ (∃!𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
207	118, 204, 206	sylanbrc 575	1 ⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 833   ∧ w3a 1068   = wceq 1507   ∈ wcel 2048  ∀wral 3082  ∃wrex 3083  ∃!wreu 3084  ⟨cop 4441   class class class wbr 4923   Or wor 5318   × cxp 5398  Oncon0 6023  suc csuc 6025  ‘cfv 6182  (class class class)co 6970  1^st c1st 7492  2^nd c2nd 7493   Er wer 8078  Ncnpi 10056   ·_N cmi 10058   <_N clti 10059   ~_Q ceq 10063  Qcnq 10064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-oadd 7901  df-omul 7902  df-er 8081  df-ni 10084  df-mi 10086  df-lti 10087  df-enq 10123  df-nq 10124

This theorem is referenced by:  nqerf  10142  enqeq  10146