Theorem recmulnq 10720

Description: Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)

Assertion

Ref	Expression
recmulnq	⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Proof of Theorem recmulnq

Dummy variables 𝑥 𝑦 𝑠 𝑟 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6787	. . . 4 ⊢ (*Q‘𝐴) ∈ V
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ V)
3		eleq1 2826	. . 3 ⊢ ((*Q‘𝐴) = 𝐵 → ((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V))
4	2, 3	syl5ibcom 244	. 2 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V))
5		id 22	. . . . . 6 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6		1nq 10684	. . . . . 6 ⊢ 1Q ∈ Q
7	5, 6	eqeltrdi 2847	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8		mulnqf 10705	. . . . . . 7 ⊢ ·Q :(Q × Q)⟶Q
9	8	fdmi 6612	. . . . . 6 ⊢ dom ·Q = (Q × Q)
10		0nnq 10680	. . . . . 6 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7458	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
12	7, 11	syl 17	. . . 4 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
13		elex 3450	. . . 4 ⊢ (𝐵 ∈ Q → 𝐵 ∈ V)
14	12, 13	simpl2im 504	. . 3 ⊢ ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V)
15	14	a1i 11	. 2 ⊢ (𝐴 ∈ Q → ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V))
16		oveq1 7282	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
17	16	eqeq1d 2740	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18		oveq2 7283	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
19	18	eqeq1d 2740	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20		nqerid 10689	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = 𝑥)
21		relxp 5607	. . . . . . . . . . . 12 ⊢ Rel (N × N)
22		elpqn 10681	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
23		1st2nd 7880	. . . . . . . . . . . 12 ⊢ ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
24	21, 22, 23	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Q → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
25	24	fveq2d 6778	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
26	20, 25	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 𝑥 = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
27	26	oveq1d 7290	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
28		mulerpq 10713	. . . . . . . 8 ⊢ (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩))
29	27, 28	eqtrdi 2794	. . . . . . 7 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
30		xp1st 7863	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
31	22, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (1st ‘𝑥) ∈ N)
32		xp2nd 7864	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
33	22, 32	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
34		mulpipq 10696	. . . . . . . . . 10 ⊢ ((((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) ∧ ((2nd ‘𝑥) ∈ N ∧ (1st ‘𝑥) ∈ N)) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩)
35	31, 33, 33, 31, 34	syl22anc 836	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩)
36		mulcompi 10652	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
37	36	opeq2i 4808	. . . . . . . . 9 ⊢ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩ = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩
38	35, 37	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
39	38	fveq2d 6778	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
40		mulclpi 10649	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
41	31, 33, 40	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
42		1nqenq 10718	. . . . . . . . . 10 ⊢ (((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
43	41, 42	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
44		elpqn 10681	. . . . . . . . . . 11 ⊢ (1Q ∈ Q → 1Q ∈ (N × N))
45	6, 44	ax-mp 5	. . . . . . . . . 10 ⊢ 1Q ∈ (N × N)
46	41, 41	opelxpd 5627	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N))
47		nqereq 10691	. . . . . . . . . 10 ⊢ ((1Q ∈ (N × N) ∧ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N)) → (1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)))
48	45, 46, 47	sylancr 587	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)))
49	43, 48	mpbid 231	. . . . . . . 8 ⊢ (𝑥 ∈ Q → ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
50		nqerid 10689	. . . . . . . . 9 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q)
51	6, 50	ax-mp 5	. . . . . . . 8 ⊢ ([Q]‘1Q) = 1Q
52	49, 51	eqtr3di 2793	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩) = 1Q)
53	29, 39, 52	3eqtrd 2782	. . . . . 6 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q)
54		fvex 6787	. . . . . . 7 ⊢ ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ∈ V
55		oveq2 7283	. . . . . . . 8 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
56	55	eqeq1d 2740	. . . . . . 7 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q))
57	54, 56	spcev 3545	. . . . . 6 ⊢ ((𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
58	53, 57	syl 17	. . . . 5 ⊢ (𝑥 ∈ Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59		mulcomnq 10709	. . . . . 6 ⊢ (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60		mulassnq 10715	. . . . . 6 ⊢ ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61		mulidnq 10719	. . . . . 6 ⊢ (𝑟 ∈ Q → (𝑟 ·Q 1Q) = 𝑟)
62	6, 9, 10, 59, 60, 61	caovmo 7509	. . . . 5 ⊢ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63		df-eu 2569	. . . . 5 ⊢ (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
64	58, 62, 63	sylanblrc 590	. . . 4 ⊢ (𝑥 ∈ Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65		cnvimass 5989	. . . . . . . 8 ⊢ (◡ ·Q “ {1Q}) ⊆ dom ·Q
66		df-rq 10673	. . . . . . . 8 ⊢ *Q = (◡ ·Q “ {1Q})
67	9	eqcomi 2747	. . . . . . . 8 ⊢ (Q × Q) = dom ·Q
68	65, 66, 67	3sstr4i 3964	. . . . . . 7 ⊢ *Q ⊆ (Q × Q)
69		relxp 5607	. . . . . . 7 ⊢ Rel (Q × Q)
70		relss 5692	. . . . . . 7 ⊢ (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
71	68, 69, 70	mp2 9	. . . . . 6 ⊢ Rel *Q
72	66	eleq2i 2830	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}))
73		ffn 6600	. . . . . . . . 9 ⊢ ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74		fniniseg 6937	. . . . . . . . 9 ⊢ ( ·Q Fn (Q × Q) → (⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)))
75	8, 73, 74	mp2b 10	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q))
76		ancom 461	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77		ancom 461	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
78		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1Q ∈ Q))
79	6, 78	mpbiri 257	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
80	9, 10	ndmovrcl 7458	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
82		opelxpi 5626	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
84	81	simpld 495	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → 𝑥 ∈ Q)
85	83, 84	2thd 264	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥 ∈ Q))
86	85	pm5.32i 575	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
87		df-ov 7278	. . . . . . . . . . . 12 ⊢ (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
88	87	eqeq1i 2743	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
89	88	anbi1i 624	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
90	77, 86, 89	3bitr2ri 300	. . . . . . . . 9 ⊢ ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
91	76, 90	bitri 274	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
92	72, 75, 91	3bitri 297	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
93	92	a1i 11	. . . . . 6 ⊢ (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
94	71, 93	opabbi2dv 5758	. . . . 5 ⊢ (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
95	94	mptru 1546	. . . 4 ⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
96	17, 19, 64, 95	fvopab3g 6870	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ V) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
97	96	ex 413	. 2 ⊢ (𝐴 ∈ Q → (𝐵 ∈ V → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
98	4, 15, 97	pm5.21ndd 381	1 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ⊤wtru 1540  ∃wex 1782   ∈ wcel 2106  ∃*wmo 2538  ∃!weu 2568  Vcvv 3432   ⊆ wss 3887  {csn 4561  ⟨cop 4567   class class class wbr 5074  {copab 5136   × cxp 5587  ^◡ccnv 5588  dom cdm 5589   “ cima 5592  Rel wrel 5594   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  1^st c1st 7829  2^nd c2nd 7830  Ncnpi 10600   ·_N cmi 10602   ·_pQ cmpq 10605   ~_Q ceq 10607  Qcnq 10608  1_Qc1q 10609  [Q]cerq 10610   ·_Q cmq 10612  *_Qcrq 10613

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

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

This theorem is referenced by:  recidnq  10721  recrecnq  10723  reclem3pr  10805