Theorem recmulnq 10917

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 6871	. . . 4 ⊢ (*Q‘𝐴) ∈ V
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ V)
3		eleq1 2816	. . 3 ⊢ ((*Q‘𝐴) = 𝐵 → ((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V))
4	2, 3	syl5ibcom 245	. 2 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V))
5		id 22	. . . . . 6 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6		1nq 10881	. . . . . 6 ⊢ 1Q ∈ Q
7	5, 6	eqeltrdi 2836	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8		mulnqf 10902	. . . . . . 7 ⊢ ·Q :(Q × Q)⟶Q
9	8	fdmi 6699	. . . . . 6 ⊢ dom ·Q = (Q × Q)
10		0nnq 10877	. . . . . 6 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7575	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
12	7, 11	syl 17	. . . 4 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
13		elex 3468	. . . 4 ⊢ (𝐵 ∈ Q → 𝐵 ∈ V)
14	12, 13	simpl2im 503	. . 3 ⊢ ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V)
15	14	a1i 11	. 2 ⊢ (𝐴 ∈ Q → ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V))
16		oveq1 7394	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
17	16	eqeq1d 2731	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18		oveq2 7395	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
19	18	eqeq1d 2731	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20		nqerid 10886	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = 𝑥)
21		relxp 5656	. . . . . . . . . . . 12 ⊢ Rel (N × N)
22		elpqn 10878	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
23		1st2nd 8018	. . . . . . . . . . . 12 ⊢ ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
24	21, 22, 23	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Q → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
25	24	fveq2d 6862	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
26	20, 25	eqtr3d 2766	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 𝑥 = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
27	26	oveq1d 7402	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
28		mulerpq 10910	. . . . . . . 8 ⊢ (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩))
29	27, 28	eqtrdi 2780	. . . . . . 7 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
30		xp1st 8000	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
31	22, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (1st ‘𝑥) ∈ N)
32		xp2nd 8001	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
33	22, 32	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
34		mulpipq 10893	. . . . . . . . . 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 838	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩)
36		mulcompi 10849	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
37	36	opeq2i 4841	. . . . . . . . 9 ⊢ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩ = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩
38	35, 37	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
39	38	fveq2d 6862	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
40		mulclpi 10846	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
41	31, 33, 40	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
42		1nqenq 10915	. . . . . . . . . 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 10878	. . . . . . . . . . 11 ⊢ (1Q ∈ Q → 1Q ∈ (N × N))
45	6, 44	ax-mp 5	. . . . . . . . . 10 ⊢ 1Q ∈ (N × N)
46	41, 41	opelxpd 5677	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N))
47		nqereq 10888	. . . . . . . . . 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 232	. . . . . . . 8 ⊢ (𝑥 ∈ Q → ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
50		nqerid 10886	. . . . . . . . 9 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q)
51	6, 50	ax-mp 5	. . . . . . . 8 ⊢ ([Q]‘1Q) = 1Q
52	49, 51	eqtr3di 2779	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩) = 1Q)
53	29, 39, 52	3eqtrd 2768	. . . . . 6 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q)
54		fvex 6871	. . . . . . 7 ⊢ ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ∈ V
55		oveq2 7395	. . . . . . . 8 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
56	55	eqeq1d 2731	. . . . . . 7 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q))
57	54, 56	spcev 3572	. . . . . 6 ⊢ ((𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
58	53, 57	syl 17	. . . . 5 ⊢ (𝑥 ∈ Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59		mulcomnq 10906	. . . . . 6 ⊢ (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60		mulassnq 10912	. . . . . 6 ⊢ ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61		mulidnq 10916	. . . . . 6 ⊢ (𝑟 ∈ Q → (𝑟 ·Q 1Q) = 𝑟)
62	6, 9, 10, 59, 60, 61	caovmo 7626	. . . . 5 ⊢ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63		df-eu 2562	. . . . 5 ⊢ (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
64	58, 62, 63	sylanblrc 590	. . . 4 ⊢ (𝑥 ∈ Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65		cnvimass 6053	. . . . . . . 8 ⊢ (◡ ·Q “ {1Q}) ⊆ dom ·Q
66		df-rq 10870	. . . . . . . 8 ⊢ *Q = (◡ ·Q “ {1Q})
67	9	eqcomi 2738	. . . . . . . 8 ⊢ (Q × Q) = dom ·Q
68	65, 66, 67	3sstr4i 3998	. . . . . . 7 ⊢ *Q ⊆ (Q × Q)
69		relxp 5656	. . . . . . 7 ⊢ Rel (Q × Q)
70		relss 5744	. . . . . . 7 ⊢ (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
71	68, 69, 70	mp2 9	. . . . . 6 ⊢ Rel *Q
72	66	eleq2i 2820	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}))
73		ffn 6688	. . . . . . . . 9 ⊢ ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74		fniniseg 7032	. . . . . . . . 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 460	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77		ancom 460	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
78		eleq1 2816	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1Q ∈ Q))
79	6, 78	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
80	9, 10	ndmovrcl 7575	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
82		opelxpi 5675	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
84	81	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → 𝑥 ∈ Q)
85	83, 84	2thd 265	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥 ∈ Q))
86	85	pm5.32i 574	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
87		df-ov 7390	. . . . . . . . . . . 12 ⊢ (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
88	87	eqeq1i 2734	. . . . . . . . . . 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 275	. . . . . . . 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 5813	. . . . 5 ⊢ (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
95	94	mptru 1547	. . . 4 ⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
96	17, 19, 64, 95	fvopab3g 6963	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ V) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
97	96	ex 412	. 2 ⊢ (𝐴 ∈ Q → (𝐵 ∈ V → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
98	4, 15, 97	pm5.21ndd 379	1 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ⊤wtru 1541  ∃wex 1779   ∈ wcel 2109  ∃*wmo 2531  ∃!weu 2561  Vcvv 3447   ⊆ wss 3914  {csn 4589  ⟨cop 4595   class class class wbr 5107  {copab 5169   × cxp 5636  ^◡ccnv 5637  dom cdm 5638   “ cima 5641  Rel wrel 5643   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  1^st c1st 7966  2^nd c2nd 7967  Ncnpi 10797   ·_N cmi 10799   ·_pQ cmpq 10802   ~_Q ceq 10804  Qcnq 10805  1_Qc1q 10806  [Q]cerq 10807   ·_Q cmq 10809  *_Qcrq 10810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-oadd 8438  df-omul 8439  df-er 8671  df-ni 10825  df-mi 10827  df-lti 10828  df-mpq 10862  df-enq 10864  df-nq 10865  df-erq 10866  df-mq 10868  df-1nq 10869  df-rq 10870

This theorem is referenced by:  recidnq  10918  recrecnq  10920  reclem3pr  11002