Theorem recmulnq 10388

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 6685	. . . 4 ⊢ (*Q‘𝐴) ∈ V
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ V)
3		eleq1 2902	. . 3 ⊢ ((*Q‘𝐴) = 𝐵 → ((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V))
4	2, 3	syl5ibcom 247	. 2 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V))
5		id 22	. . . . . 6 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6		1nq 10352	. . . . . 6 ⊢ 1Q ∈ Q
7	5, 6	eqeltrdi 2923	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8		mulnqf 10373	. . . . . . 7 ⊢ ·Q :(Q × Q)⟶Q
9	8	fdmi 6526	. . . . . 6 ⊢ dom ·Q = (Q × Q)
10		0nnq 10348	. . . . . 6 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7336	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
12	7, 11	syl 17	. . . 4 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
13		elex 3514	. . . 4 ⊢ (𝐵 ∈ Q → 𝐵 ∈ V)
14	12, 13	simpl2im 506	. . 3 ⊢ ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V)
15	14	a1i 11	. 2 ⊢ (𝐴 ∈ Q → ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V))
16		oveq1 7165	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
17	16	eqeq1d 2825	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18		oveq2 7166	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
19	18	eqeq1d 2825	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20		nqerid 10357	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = 𝑥)
21		relxp 5575	. . . . . . . . . . . 12 ⊢ Rel (N × N)
22		elpqn 10349	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
23		1st2nd 7740	. . . . . . . . . . . 12 ⊢ ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
24	21, 22, 23	sylancr 589	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Q → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
25	24	fveq2d 6676	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
26	20, 25	eqtr3d 2860	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 𝑥 = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
27	26	oveq1d 7173	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
28		mulerpq 10381	. . . . . . . 8 ⊢ (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩))
29	27, 28	syl6eq 2874	. . . . . . 7 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
30		xp1st 7723	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
31	22, 30	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (1st ‘𝑥) ∈ N)
32		xp2nd 7724	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
33	22, 32	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
34		mulpipq 10364	. . . . . . . . . 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 10320	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
37	36	opeq2i 4809	. . . . . . . . 9 ⊢ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩ = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩
38	35, 37	syl6eq 2874	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
39	38	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
40		nqerid 10357	. . . . . . . . 9 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q)
41	6, 40	ax-mp 5	. . . . . . . 8 ⊢ ([Q]‘1Q) = 1Q
42		mulclpi 10317	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
43	31, 33, 42	syl2anc 586	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
44		1nqenq 10386	. . . . . . . . . 10 ⊢ (((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
45	43, 44	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
46		elpqn 10349	. . . . . . . . . . 11 ⊢ (1Q ∈ Q → 1Q ∈ (N × N))
47	6, 46	ax-mp 5	. . . . . . . . . 10 ⊢ 1Q ∈ (N × N)
48	43, 43	opelxpd 5595	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N))
49		nqereq 10359	. . . . . . . . . 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 ‘𝑥))⟩)))
50	47, 48, 49	sylancr 589	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)))
51	45, 50	mpbid 234	. . . . . . . 8 ⊢ (𝑥 ∈ Q → ([Q]‘1Q) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
52	41, 51	syl5reqr 2873	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩) = 1Q)
53	29, 39, 52	3eqtrd 2862	. . . . . 6 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q)
54		fvex 6685	. . . . . . 7 ⊢ ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ∈ V
55		oveq2 7166	. . . . . . . 8 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
56	55	eqeq1d 2825	. . . . . . 7 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q))
57	54, 56	spcev 3609	. . . . . 6 ⊢ ((𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
58	53, 57	syl 17	. . . . 5 ⊢ (𝑥 ∈ Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59		mulcomnq 10377	. . . . . 6 ⊢ (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60		mulassnq 10383	. . . . . 6 ⊢ ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61		mulidnq 10387	. . . . . 6 ⊢ (𝑟 ∈ Q → (𝑟 ·Q 1Q) = 𝑟)
62	6, 9, 10, 59, 60, 61	caovmo 7387	. . . . 5 ⊢ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63		df-eu 2654	. . . . 5 ⊢ (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
64	58, 62, 63	sylanblrc 592	. . . 4 ⊢ (𝑥 ∈ Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65		cnvimass 5951	. . . . . . . 8 ⊢ (◡ ·Q “ {1Q}) ⊆ dom ·Q
66		df-rq 10341	. . . . . . . 8 ⊢ *Q = (◡ ·Q “ {1Q})
67	9	eqcomi 2832	. . . . . . . 8 ⊢ (Q × Q) = dom ·Q
68	65, 66, 67	3sstr4i 4012	. . . . . . 7 ⊢ *Q ⊆ (Q × Q)
69		relxp 5575	. . . . . . 7 ⊢ Rel (Q × Q)
70		relss 5658	. . . . . . 7 ⊢ (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
71	68, 69, 70	mp2 9	. . . . . 6 ⊢ Rel *Q
72	66	eleq2i 2906	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}))
73		ffn 6516	. . . . . . . . 9 ⊢ ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74		fniniseg 6832	. . . . . . . . 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 463	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77		ancom 463	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
78		eleq1 2902	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1Q ∈ Q))
79	6, 78	mpbiri 260	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
80	9, 10	ndmovrcl 7336	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
82		opelxpi 5594	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
84	81	simpld 497	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → 𝑥 ∈ Q)
85	83, 84	2thd 267	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥 ∈ Q))
86	85	pm5.32i 577	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
87		df-ov 7161	. . . . . . . . . . . 12 ⊢ (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
88	87	eqeq1i 2828	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
89	88	anbi1i 625	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
90	77, 86, 89	3bitr2ri 302	. . . . . . . . 9 ⊢ ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
91	76, 90	bitri 277	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
92	72, 75, 91	3bitri 299	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q))
93	92	a1i 11	. . . . . 6 ⊢ (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
94	71, 93	opabbi2dv 5722	. . . . 5 ⊢ (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
95	94	mptru 1544	. . . 4 ⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
96	17, 19, 64, 95	fvopab3g 6765	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ V) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
97	96	ex 415	. 2 ⊢ (𝐴 ∈ Q → (𝐵 ∈ V → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
98	4, 15, 97	pm5.21ndd 383	1 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ⊤wtru 1538  ∃wex 1780   ∈ wcel 2114  ∃*wmo 2620  ∃!weu 2653  Vcvv 3496   ⊆ wss 3938  {csn 4569  ⟨cop 4575   class class class wbr 5068  {copab 5130   × cxp 5555  ^◡ccnv 5556  dom cdm 5557   “ cima 5560  Rel wrel 5562   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  1^st c1st 7689  2^nd c2nd 7690  Ncnpi 10268   ·_N cmi 10270   ·_pQ cmpq 10273   ~_Q ceq 10275  Qcnq 10276  1_Qc1q 10277  [Q]cerq 10278   ·_Q cmq 10280  *_Qcrq 10281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-omul 8109  df-er 8291  df-ni 10296  df-mi 10298  df-lti 10299  df-mpq 10333  df-enq 10335  df-nq 10336  df-erq 10337  df-mq 10339  df-1nq 10340  df-rq 10341

This theorem is referenced by:  recidnq  10389  recrecnq  10391  reclem3pr  10473