Theorem nqereu 9630

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 5056	. . 3 ⊢ (𝐴 ∈ (N × N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩)
2		pion 9580	. . . . . . . . 9 ⊢ (𝑏 ∈ N → 𝑏 ∈ On)
3		suceloni 6905	. . . . . . . . 9 ⊢ (𝑏 ∈ On → suc 𝑏 ∈ On)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑏 ∈ N → suc 𝑏 ∈ On)
5		vex 3176	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6	5	sucid 5721	. . . . . . . 8 ⊢ 𝑏 ∈ suc 𝑏
7		eleq2 2677	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏))
8	7	rspcev 3282	. . . . . . . 8 ⊢ ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
9	4, 6, 8	sylancl 693	. . . . . . 7 ⊢ (𝑏 ∈ N → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
10	9	adantl 481	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦)
11		elequ2 1991	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚))
12	11	imbi1d 330	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
13	12	2ralbidv 2972	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
14		opeq1 4340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
15	14	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑑⟩))
16	15	rexbidv 3034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩))
17	16	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩)))
18		elequ1 1984	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
19		opeq2 4341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
20	19	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
21	20	rexbidv 3034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
22	18, 21	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑑⟩) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
23	17, 22	cbvral2v 3155	. . . . . . . . . . . . . . 15 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
24	23	ralbii 2963	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
25		rexnal 2978	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏))
26		pm4.63 436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏))
27		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (N × N) → (2nd ‘𝑧) ∈ N)
28		ltpiord 9588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
29	28	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 ∈ N ∧ (2nd ‘𝑧) ∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
30	27, 29	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ N ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
31	30	adantll 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
32	31	anbi2d 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
33	26, 32	syl5bb 271	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
34	33	rexbidva 3031	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
35	25, 34	syl5bbr 273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏)))
36		xp1st 7089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (N × N) → (1st ‘𝑧) ∈ N)
37		elequ2 1991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏))
38	37	imbi1d 330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
39	38	2ralbidv 2972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
40	39	rspccv 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩)))
41		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑐 = (1st ‘𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st ‘𝑧), 𝑑⟩)
42	41	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
43	42	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩))
44	43	imbi2d 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
45	44	ralbidv 2969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
46	45	rspccv 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩)))
47		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏))
48		opeq2 4341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑑 = (2nd ‘𝑧) → ⟨(1st ‘𝑧), 𝑑⟩ = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
49	48	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
50	49	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = (2nd ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩ ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
51	47, 50	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = (2nd ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) ↔ ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
52	51	rspccv 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), 𝑑⟩) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
53	46, 52	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
54	40, 53	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))))
55	54	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → ((1st ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
56	36, 55	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))))
57	27, 56	mpdi 44	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N × N) → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
58	57	3imp 1249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
59		1st2nd2 7096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
60	59	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
61	60	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (N × N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
62	61	3ad2ant2 1076	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
63	58, 62	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧)
64		enqer 9622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ~Q Er (N × N)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ~Q Er (N × N))
66		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
68	65, 66, 67	ertr4d 7648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q ⟨𝑎, 𝑏⟩)
69	68	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q ⟨𝑎, 𝑏⟩))
70	69	reximdv 2999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
71	63, 70	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
72	71	3expia 1259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd ‘𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
73	72	com23 84	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
74	73	impd 446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
75	74	rexlimdva 3013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
76	75	ex 449	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
77	76	com3r 85	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
78	35, 77	syl6bi 242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
79	78	com13 86	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
80		mulcompi 9597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
81		enqbreq 9620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑎 ∈ N ∧ 𝑏 ∈ N)) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
82	81	anidms 675	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
83	80, 82	mpbiri 247	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩)
84		opelxpi 5072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
85		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
86		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
87	86, 5	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
88	87	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N 𝑏))
89	88	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N 𝑏))
90	85, 89	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
91	90	ralbidv 2969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
92		df-nq 9613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))}
93	91, 92	elrab2 3333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏)))
94	93	simplbi2 653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ (N × N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
95	84, 94	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
96		breq1 4586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩))
97	96	rspcev 3282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
98	97	expcom 450	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑏⟩ ~Q ⟨𝑎, 𝑏⟩ → (⟨𝑎, 𝑏⟩ ∈ Q → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
99	83, 95, 98	sylsyld 59	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
100	99	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
101	100	a1dd 48	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd ‘𝑧) <N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
102	79, 101	pm2.61d2 171	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
103	102	ralrimivv 2953	. . . . . . . . . . . . . 14 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑐, 𝑑⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
104	24, 103	sylbir 224	. . . . . . . . . . . . 13 ⊢ (∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
105	104	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
106	13, 105	tfis2 6948	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
107		rsp 2913	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
108	106, 107	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
109		rsp 2913	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
110	108, 109	syl6 34	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (𝑎 ∈ N → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))))
111	110	impd 446	. . . . . . . 8 ⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
112	111	com12 32	. . . . . . 7 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝑦 ∈ On → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)))
113	112	rexlimdv 3012	. . . . . 6 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (∃𝑦 ∈ On 𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
114	10, 113	mpd 15	. . . . 5 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩)
115		breq2 4587	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q ⟨𝑎, 𝑏⟩))
116	115	rexbidv 3034	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q ⟨𝑎, 𝑏⟩))
117	114, 116	syl5ibrcom 236	. . . 4 ⊢ ((𝑎 ∈ N ∧ 𝑏 ∈ N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴))
118	117	rexlimivv 3018	. . 3 ⊢ (∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
119	1, 118	sylbi 206	. 2 ⊢ (𝐴 ∈ (N × N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)
120		breq2 4587	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴))
121		breq2 4587	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴))
122	120, 121	anbi12d 743	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴)))
123	122	imbi1d 330	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
124	123	2ralbidv 2972	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
125	64	a1i 11	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → ~Q Er (N × N))
126		simpl 472	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
127		simpr 476	. . . . . 6 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
128	125, 126, 127	ertr4d 7648	. . . . 5 ⊢ ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
129		mulcompi 9597	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
130		elpqn 9626	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Q → 𝑦 ∈ (N × N))
131		breq1 4586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧))
132		fveq2 6103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥))
133	132	breq2d 4595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑧) <N (2nd ‘𝑥)))
134	133	notbid 307	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
135	131, 134	imbi12d 333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
136	135	ralbidv 2969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
137	136, 92	elrab2 3333	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))))
138	137	simprbi 479	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)))
139		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦))
140		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦))
141	140	breq1d 4593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N (2nd ‘𝑥) ↔ (2nd ‘𝑦) <N (2nd ‘𝑥)))
142	141	notbid 307	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑥) ↔ ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
143	139, 142	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))))
144	143	rspcva 3280	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
145	130, 138, 144	syl2anr 494	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥)))
146	145	imp 444	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))
147	64	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ~Q 𝑦 → ~Q Er (N × N))
148		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ~Q 𝑦 → 𝑥 ~Q 𝑦)
149	147, 148	ersym 7641	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ~Q 𝑦 → 𝑦 ~Q 𝑥)
150		elpqn 9626	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
151	92	rabeq2i 3170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))))
152	151	simprbi 479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)))
153		breq2 4587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥))
154		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥))
155	154	breq1d 4593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N (2nd ‘𝑦) ↔ (2nd ‘𝑥) <N (2nd ‘𝑦)))
156	155	notbid 307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
157	153, 156	imbi12d 333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))))
158	157	rspcva 3280	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd ‘𝑧) <N (2nd ‘𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
159	150, 152, 158	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
160	149, 159	syl5 33	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦)))
161	160	imp 444	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))
162		xp2nd 7090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
163	150, 162	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
164	163	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) ∈ N)
165		xp2nd 7090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (N × N) → (2nd ‘𝑦) ∈ N)
166	130, 165	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ Q → (2nd ‘𝑦) ∈ N)
167	166	ad2antlr 759	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑦) ∈ N)
168		ltsopi 9589	. . . . . . . . . . . . . . . . . . 19 ⊢ <N Or N
169		sotric 4985	. . . . . . . . . . . . . . . . . . 19 ⊢ (( <N Or N ∧ ((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
170	168, 169	mpan 702	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → ((2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
171	170	notbid 307	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
172		notnotb 303	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)) ↔ ¬ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
173	171, 172	syl6bbr 277	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘𝑥) ∈ N ∧ (2nd ‘𝑦) ∈ N) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
174	164, 167, 173	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) <N (2nd ‘𝑦) ↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥))))
175	161, 174	mpbid 221	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N (2nd ‘𝑥)))
176	175	ord 391	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd ‘𝑦) <N (2nd ‘𝑥)))
177	146, 176	mt3d 139	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦))
178	177	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
179	129, 178	syl5eq 2656	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑦)))
180		1st2nd2 7096	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
181		1st2nd2 7096	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
182	180, 181	breqan12d 4599	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
183		xp1st 7089	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
184	183, 162	jca 553	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (N × N) → ((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N))
185		xp1st 7089	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (N × N) → (1st ‘𝑦) ∈ N)
186	185, 165	jca 553	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (N × N) → ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N))
187		enqbreq 9620	. . . . . . . . . . . . . 14 ⊢ ((((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) ∧ ((1st ‘𝑦) ∈ N ∧ (2nd ‘𝑦) ∈ N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
188	184, 186, 187	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ~Q ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
189	182, 188	bitrd 267	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
190	150, 130, 189	syl2an 493	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 ↔ ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦))))
191	190	biimpa 500	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((1st ‘𝑥) ·N (2nd ‘𝑦)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
192	179, 191	eqtrd 2644	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)))
193	150	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
194		mulcanpi 9601	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
195	162, 183, 194	syl2anc 691	. . . . . . . . . 10 ⊢ (𝑥 ∈ (N × N) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
196	193, 195	syl 17	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((2nd ‘𝑥) ·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦)))
197	192, 196	mpbid 221	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦))
198	197, 177	opeq12d 4348	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
199	193, 180	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
200	130	ad2antlr 759	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
201	200, 181	syl 17	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
202	198, 199, 201	3eqtr4d 2654	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
203	202	ex 449	. . . . 5 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥 ~Q 𝑦 → 𝑥 = 𝑦))
204	128, 203	syl5 33	. . . 4 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
205	204	rgen2a 2960	. . 3 ⊢ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
206	124, 205	vtoclg 3239	. 2 ⊢ (𝐴 ∈ (N × N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
207		breq1 4586	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴))
208	207	reu4 3367	. 2 ⊢ (∃!𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
209	119, 206, 208	sylanbrc 695	1 ⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ⟨cop 4131   class class class wbr 4583   Or wor 4958   × cxp 5036  Oncon0 5640  suc csuc 5642  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058   Er wer 7626  Ncnpi 9545   ·_N cmi 9547   <_N clti 9548   ~_Q ceq 9552  Qcnq 9553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-oadd 7451  df-omul 7452  df-er 7629  df-ni 9573  df-mi 9575  df-lti 9576  df-enq 9612  df-nq 9613

This theorem is referenced by:  nqerf  9631  enqeq  9635