Theorem recmulnq 10543

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 6708	. . . 4 ⊢ (*Q‘𝐴) ∈ V
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ V)
3		eleq1 2818	. . 3 ⊢ ((*Q‘𝐴) = 𝐵 → ((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V))
4	2, 3	syl5ibcom 248	. 2 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V))
5		id 22	. . . . . 6 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6		1nq 10507	. . . . . 6 ⊢ 1Q ∈ Q
7	5, 6	eqeltrdi 2839	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8		mulnqf 10528	. . . . . . 7 ⊢ ·Q :(Q × Q)⟶Q
9	8	fdmi 6535	. . . . . 6 ⊢ dom ·Q = (Q × Q)
10		0nnq 10503	. . . . . 6 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7372	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
12	7, 11	syl 17	. . . 4 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
13		elex 3416	. . . 4 ⊢ (𝐵 ∈ Q → 𝐵 ∈ V)
14	12, 13	simpl2im 507	. . 3 ⊢ ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V)
15	14	a1i 11	. 2 ⊢ (𝐴 ∈ Q → ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V))
16		oveq1 7198	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
17	16	eqeq1d 2738	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18		oveq2 7199	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
19	18	eqeq1d 2738	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20		nqerid 10512	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = 𝑥)
21		relxp 5554	. . . . . . . . . . . 12 ⊢ Rel (N × N)
22		elpqn 10504	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
23		1st2nd 7788	. . . . . . . . . . . 12 ⊢ ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
24	21, 22, 23	sylancr 590	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Q → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
25	24	fveq2d 6699	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
26	20, 25	eqtr3d 2773	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 𝑥 = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
27	26	oveq1d 7206	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
28		mulerpq 10536	. . . . . . . 8 ⊢ (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩))
29	27, 28	eqtrdi 2787	. . . . . . 7 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
30		xp1st 7771	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
31	22, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (1st ‘𝑥) ∈ N)
32		xp2nd 7772	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
33	22, 32	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
34		mulpipq 10519	. . . . . . . . . 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 839	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩)
36		mulcompi 10475	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
37	36	opeq2i 4774	. . . . . . . . 9 ⊢ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩ = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩
38	35, 37	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
39	38	fveq2d 6699	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
40		mulclpi 10472	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
41	31, 33, 40	syl2anc 587	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
42		1nqenq 10541	. . . . . . . . . 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 10504	. . . . . . . . . . 11 ⊢ (1Q ∈ Q → 1Q ∈ (N × N))
45	6, 44	ax-mp 5	. . . . . . . . . 10 ⊢ 1Q ∈ (N × N)
46	41, 41	opelxpd 5574	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N))
47		nqereq 10514	. . . . . . . . . 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 590	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)))
49	43, 48	mpbid 235	. . . . . . . 8 ⊢ (𝑥 ∈ Q → ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
50		nqerid 10512	. . . . . . . . 9 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q)
51	6, 50	ax-mp 5	. . . . . . . 8 ⊢ ([Q]‘1Q) = 1Q
52	49, 51	eqtr3di 2786	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩) = 1Q)
53	29, 39, 52	3eqtrd 2775	. . . . . 6 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q)
54		fvex 6708	. . . . . . 7 ⊢ ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ∈ V
55		oveq2 7199	. . . . . . . 8 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
56	55	eqeq1d 2738	. . . . . . 7 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q))
57	54, 56	spcev 3511	. . . . . 6 ⊢ ((𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
58	53, 57	syl 17	. . . . 5 ⊢ (𝑥 ∈ Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59		mulcomnq 10532	. . . . . 6 ⊢ (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60		mulassnq 10538	. . . . . 6 ⊢ ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61		mulidnq 10542	. . . . . 6 ⊢ (𝑟 ∈ Q → (𝑟 ·Q 1Q) = 𝑟)
62	6, 9, 10, 59, 60, 61	caovmo 7423	. . . . 5 ⊢ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63		df-eu 2568	. . . . 5 ⊢ (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
64	58, 62, 63	sylanblrc 593	. . . 4 ⊢ (𝑥 ∈ Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65		cnvimass 5934	. . . . . . . 8 ⊢ (◡ ·Q “ {1Q}) ⊆ dom ·Q
66		df-rq 10496	. . . . . . . 8 ⊢ *Q = (◡ ·Q “ {1Q})
67	9	eqcomi 2745	. . . . . . . 8 ⊢ (Q × Q) = dom ·Q
68	65, 66, 67	3sstr4i 3930	. . . . . . 7 ⊢ *Q ⊆ (Q × Q)
69		relxp 5554	. . . . . . 7 ⊢ Rel (Q × Q)
70		relss 5638	. . . . . . 7 ⊢ (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
71	68, 69, 70	mp2 9	. . . . . 6 ⊢ Rel *Q
72	66	eleq2i 2822	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}))
73		ffn 6523	. . . . . . . . 9 ⊢ ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74		fniniseg 6858	. . . . . . . . 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 464	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77		ancom 464	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
78		eleq1 2818	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1Q ∈ Q))
79	6, 78	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
80	9, 10	ndmovrcl 7372	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
82		opelxpi 5573	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
84	81	simpld 498	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → 𝑥 ∈ Q)
85	83, 84	2thd 268	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥 ∈ Q))
86	85	pm5.32i 578	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
87		df-ov 7194	. . . . . . . . . . . 12 ⊢ (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
88	87	eqeq1i 2741	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
89	88	anbi1i 627	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
90	77, 86, 89	3bitr2ri 303	. . . . . . . . 9 ⊢ ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
91	76, 90	bitri 278	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
92	72, 75, 91	3bitri 300	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
93	92	a1i 11	. . . . . 6 ⊢ (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
94	71, 93	opabbi2dv 5703	. . . . 5 ⊢ (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
95	94	mptru 1550	. . . 4 ⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
96	17, 19, 64, 95	fvopab3g 6791	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ V) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
97	96	ex 416	. 2 ⊢ (𝐴 ∈ Q → (𝐵 ∈ V → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
98	4, 15, 97	pm5.21ndd 384	1 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ⊤wtru 1544  ∃wex 1787   ∈ wcel 2112  ∃*wmo 2537  ∃!weu 2567  Vcvv 3398   ⊆ wss 3853  {csn 4527  ⟨cop 4533   class class class wbr 5039  {copab 5101   × cxp 5534  ^◡ccnv 5535  dom cdm 5536   “ cima 5539  Rel wrel 5541   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7191  1^st c1st 7737  2^nd c2nd 7738  Ncnpi 10423   ·_N cmi 10425   ·_pQ cmpq 10428   ~_Q ceq 10430  Qcnq 10431  1_Qc1q 10432  [Q]cerq 10433   ·_Q cmq 10435  *_Qcrq 10436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-1o 8180  df-oadd 8184  df-omul 8185  df-er 8369  df-ni 10451  df-mi 10453  df-lti 10454  df-mpq 10488  df-enq 10490  df-nq 10491  df-erq 10492  df-mq 10494  df-1nq 10495  df-rq 10496

This theorem is referenced by:  recidnq  10544  recrecnq  10546  reclem3pr  10628