Theorem recmulnq 10976

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 6895	. . . 4 ⊢ (*Q‘𝐴) ∈ V
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ V)
3		eleq1 2850	. . 3 ⊢ ((*Q‘𝐴) = 𝐵 → ((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V))
4	2, 3	syl5ibcom 248	. 2 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V))
5		id 23	. . . . . 6 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6		1nq 10940	. . . . . 6 ⊢ 1Q ∈ Q
7	5, 6	eqeltrdi 2870	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8		mulnqf 10961	. . . . . . 7 ⊢ ·Q :(Q × Q)⟶Q
9	8	fdmi 6718	. . . . . 6 ⊢ dom ·Q = (Q × Q)
10		0nnq 10936	. . . . . 6 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7603	. . . . 5 ⊢ ((𝐴 ·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
12	7, 11	syl 18	. . . 4 ⊢ ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ∈ Q ∧ 𝐵 ∈ Q))
13		elex 3474	. . . 4 ⊢ (𝐵 ∈ Q → 𝐵 ∈ V)
14	12, 13	simpl2im 513	. . 3 ⊢ ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V)
15	14	a1i 11	. 2 ⊢ (𝐴 ∈ Q → ((𝐴 ·Q 𝐵) = 1Q → 𝐵 ∈ V))
16		oveq1 7423	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
17	16	eqeq1d 2764	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18		oveq2 7424	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
19	18	eqeq1d 2764	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20		nqerid 10945	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = 𝑥)
21		relxp 5677	. . . . . . . . . . . 12 ⊢ Rel (N × N)
22		elpqn 10937	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N))
23		1st2nd 8039	. . . . . . . . . . . 12 ⊢ ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
24	21, 22, 23	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Q → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
25	24	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ([Q]‘𝑥) = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
26	20, 25	eqtr3d 2799	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 𝑥 = ([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
27	26	oveq1d 7431	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
28		mulerpq 10969	. . . . . . . 8 ⊢ (([Q]‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩))
29	27, 28	eqtrdi 2813	. . . . . . 7 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
30		xp1st 8021	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (1st ‘𝑥) ∈ N)
31	22, 30	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (1st ‘𝑥) ∈ N)
32		xp2nd 8022	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (N × N) → (2nd ‘𝑥) ∈ N)
33	22, 32	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → (2nd ‘𝑥) ∈ N)
34		mulpipq 10952	. . . . . . . . . 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 852	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩)
36		mulcompi 10908	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ·N (1st ‘𝑥)) = ((1st ‘𝑥) ·N (2nd ‘𝑥))
37	36	opeq2i 4840	. . . . . . . . 9 ⊢ ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((2nd ‘𝑥) ·N (1st ‘𝑥))⟩ = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩
38	35, 37	eqtrdi 2813	. . . . . . . 8 ⊢ (𝑥 ∈ Q → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) = ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
39	38	fveq2d 6886	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ·pQ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩))
40		mulclpi 10905	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) ∈ N ∧ (2nd ‘𝑥) ∈ N) → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
41	31, 33, 40	syl2anc 596	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N)
42		1nqenq 10974	. . . . . . . . . 10 ⊢ (((1st ‘𝑥) ·N (2nd ‘𝑥)) ∈ N → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
43	41, 42	syl 18	. . . . . . . . 9 ⊢ (𝑥 ∈ Q → 1Q ~Q ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩)
44		elpqn 10937	. . . . . . . . . . 11 ⊢ (1Q ∈ Q → 1Q ∈ (N × N))
45	6, 44	ax-mp 5	. . . . . . . . . 10 ⊢ 1Q ∈ (N × N)
46	41, 41	opelxpd 5698	. . . . . . . . . 10 ⊢ (𝑥 ∈ Q → ⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩ ∈ (N × N))
47		nqereq 10947	. . . . . . . . . 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 599	. . . . . . . . 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 10945	. . . . . . . . 9 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q)
51	6, 50	ax-mp 5	. . . . . . . 8 ⊢ ([Q]‘1Q) = 1Q
52	49, 51	eqtr3di 2812	. . . . . . 7 ⊢ (𝑥 ∈ Q → ([Q]‘⟨((1st ‘𝑥) ·N (2nd ‘𝑥)), ((1st ‘𝑥) ·N (2nd ‘𝑥))⟩) = 1Q)
53	29, 39, 52	3eqtrd 2801	. . . . . 6 ⊢ (𝑥 ∈ Q → (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q)
54		fvex 6895	. . . . . . 7 ⊢ ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ∈ V
55		oveq2 7424	. . . . . . . 8 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)))
56	55	eqeq1d 2764	. . . . . . 7 ⊢ (𝑦 = ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q))
57	54, 56	spcev 3563	. . . . . 6 ⊢ ((𝑥 ·Q ([Q]‘⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
58	53, 57	syl 18	. . . . 5 ⊢ (𝑥 ∈ Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59		mulcomnq 10965	. . . . . 6 ⊢ (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60		mulassnq 10971	. . . . . 6 ⊢ ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61		mulidnq 10975	. . . . . 6 ⊢ (𝑟 ∈ Q → (𝑟 ·Q 1Q) = 𝑟)
62	6, 9, 10, 59, 60, 61	caovmo 7654	. . . . 5 ⊢ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63		df-eu 2596	. . . . 5 ⊢ (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
64	58, 62, 63	sylanblrc 602	. . . 4 ⊢ (𝑥 ∈ Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65		cnvimass 6082	. . . . . . . 8 ⊢ (◡ ·Q “ {1Q}) ⊆ dom ·Q
66		df-rq 10929	. . . . . . . 8 ⊢ *Q = (◡ ·Q “ {1Q})
67	9	eqcomi 2771	. . . . . . . 8 ⊢ (Q × Q) = dom ·Q
68	65, 66, 67	3sstr4i 3985	. . . . . . 7 ⊢ *Q ⊆ (Q × Q)
69		relxp 5677	. . . . . . 7 ⊢ Rel (Q × Q)
70		relss 5766	. . . . . . 7 ⊢ (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
71	68, 69, 70	mp2 9	. . . . . 6 ⊢ Rel *Q
72	66	eleq2i 2854	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ (◡ ·Q “ {1Q}))
73		ffn 6706	. . . . . . . . 9 ⊢ ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74		fniniseg 7056	. . . . . . . . 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 466	. . . . . . . . 9 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77		ancom 466	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
78		eleq1 2850	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1Q ∈ Q))
79	6, 78	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
80	9, 10	ndmovrcl 7603	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
81	79, 80	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧ 𝑦 ∈ Q))
82		opelxpi 5696	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
83	81, 82	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
84	81	simpld 500	. . . . . . . . . . . 12 ⊢ ((𝑥 ·Q 𝑦) = 1Q → 𝑥 ∈ Q)
85	83, 84	2thd 268	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥 ∈ Q))
86	85	pm5.32i 585	. . . . . . . . . 10 ⊢ (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q ∧ 𝑥 ∈ Q))
87		df-ov 7419	. . . . . . . . . . . 12 ⊢ (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
88	87	eqeq1i 2767	. . . . . . . . . . 11 ⊢ ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
89	88	anbi1i 636	. . . . . . . . . 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 5833	. . . . 5 ⊢ (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
95	94	mptru 1577	. . . 4 ⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
96	17, 19, 64, 95	fvopab3g 6985	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ V) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
97	96	ex 418	. 2 ⊢ (𝐴 ∈ Q → (𝐵 ∈ V → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
98	4, 15, 97	pm5.21ndd 382	1 ⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2564  ∃!weu 2595  Vcvv 3453   ⊆ wss 3902  {csn 4587  ⟨cop 4593   class class class wbr 5107  {copab 5171   × cxp 5657  ^◡ccnv 5658  dom cdm 5659   “ cima 5662  Rel wrel 5664   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  1^st c1st 7987  2^nd c2nd 7988  Ncnpi 10856   ·_N cmi 10858   ·_pQ cmpq 10861   ~_Q ceq 10863  Qcnq 10864  1_Qc1q 10865  [Q]cerq 10866   ·_Q cmq 10868  *_Qcrq 10869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-oadd 8462  df-omul 8463  df-er 8699  df-ni 10884  df-mi 10886  df-lti 10887  df-mpq 10921  df-enq 10923  df-nq 10924  df-erq 10925  df-mq 10927  df-1nq 10928  df-rq 10929

This theorem is used by:  recidnq  10977  recrecnq  10979  reclem3pr  11061