hoicvr - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hoicvr		Structured version Visualization version Unicode version

Theorem hoicvr 38488

Description:

is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
hoicvr.2
hoicvr.3

**Assertion**
Ref	Expression
hoicvr

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem hoicvr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reex 9648	. . . . . . 7
2		mapdm0 37542	. . . . . . 7
3	1, 2	ax-mp 5	. . . . . 6
4	3	a1i 11	. . . . 5
5		oveq2 6316	. . . . 5
6		ixpeq1 7551	. . . . . . 7
7	6	iuneq2d 4296	. . . . . 6
8		ixp0x 7568	. . . . . . . . . 10
9	8	a1i 11	. . . . . . . . 9
10	9	iuneq2i 4288	. . . . . . . 8
11		1nn 10642	. . . . . . . . . 10
12	11	ne0ii 3729	. . . . . . . . 9
13		iunconst 4278	. . . . . . . . 9
14	12, 13	ax-mp 5	. . . . . . . 8
15	10, 14	eqtri 2493	. . . . . . 7
16	15	a1i 11	. . . . . 6
17	7, 16	eqtrd 2505	. . . . 5
18	4, 5, 17	3eqtr4d 2515	. . . 4
19		eqimss 3470	. . . 4
20	18, 19	syl 17	. . 3
21	20	adantl 473	. 2 $/\$
22		simpll 768	. . . . . 6 $/\$ $/\$
23		simpr 468	. . . . . 6 $/\$ $/\$
24		simplr 770	. . . . . 6 $/\$ $/\$
25		rncoss 5101	. . . . . . . . . . 11
26		absf 13477	. . . . . . . . . . . 12
27		frn 5747	. . . . . . . . . . . 12
28	26, 27	ax-mp 5	. . . . . . . . . . 11
29	25, 28	sstri 3427	. . . . . . . . . 10
30	29	a1i 11	. . . . . . . . 9 $/\$ $/\$
31		ltso 9732	. . . . . . . . . . 11
32	31	a1i 11	. . . . . . . . . 10 $/\$ $/\$
33	26	a1i 11	. . . . . . . . . . . . 13 $/\$
34		elmapi 7511	. . . . . . . . . . . . . . 15
35	34	adantl 473	. . . . . . . . . . . . . 14 $/\$
36		ax-resscn 9614	. . . . . . . . . . . . . . 15
37	36	a1i 11	. . . . . . . . . . . . . 14 $/\$
38	35, 37	fssd 5750	. . . . . . . . . . . . 13 $/\$
39		fco 5751	. . . . . . . . . . . . 13 $/\$
40	33, 38, 39	syl2anc 673	. . . . . . . . . . . 12 $/\$
41		hoicvr.3	. . . . . . . . . . . . 13
42	41	adantr 472	. . . . . . . . . . . 12 $/\$
43		rnffi 37513	. . . . . . . . . . . 12 $/\$
44	40, 42, 43	syl2anc 673	. . . . . . . . . . 11 $/\$
45	44	adantr 472	. . . . . . . . . 10 $/\$ $/\$
46		frn 5747	. . . . . . . . . . . . . . . . . . . 20
47	34, 46	syl 17	. . . . . . . . . . . . . . . . . . 19
48	26	fdmi 5746	. . . . . . . . . . . . . . . . . . . . . 22
49	48	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . 21
50	36, 49	sseqtri 3450	. . . . . . . . . . . . . . . . . . . 20
51	50	a1i 11	. . . . . . . . . . . . . . . . . . 19
52	47, 51	sstrd 3428	. . . . . . . . . . . . . . . . . 18
53		dmcosseq 5102	. . . . . . . . . . . . . . . . . 18
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17
55		fdm 5745	. . . . . . . . . . . . . . . . . 18
56	34, 55	syl 17	. . . . . . . . . . . . . . . . 17
57	54, 56	eqtrd 2505	. . . . . . . . . . . . . . . 16
58	57	adantr 472	. . . . . . . . . . . . . . 15 $/\$
59		neqne 2651	. . . . . . . . . . . . . . . 16
60	59	adantl 473	. . . . . . . . . . . . . . 15 $/\$
61	58, 60	eqnetrd 2710	. . . . . . . . . . . . . 14 $/\$
62	61	neneqd 2648	. . . . . . . . . . . . 13 $/\$
63		dm0rn0 5057	. . . . . . . . . . . . 13
64	62, 63	sylnib 311	. . . . . . . . . . . 12 $/\$
65	64	neqned 2650	. . . . . . . . . . 11 $/\$
66	65	adantll 728	. . . . . . . . . 10 $/\$ $/\$
67		fisupcl 8003	. . . . . . . . . 10 $/\$ $/\$ $/\$
68	32, 45, 66, 30, 67	syl13anc 1294	. . . . . . . . 9 $/\$ $/\$
69	30, 68	sseldd 3419	. . . . . . . 8 $/\$ $/\$
70		arch 10890	. . . . . . . 8
71	69, 70	syl 17	. . . . . . 7 $/\$ $/\$
72	35	ffnd 5740	. . . . . . . . . . . . 13 $/\$
73	72	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
74	73	adantlr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
75		simplll 776	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
76		id 22	. . . . . . . . . . . . . . . . 17
77	76	ad3antlr 745	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
78		simplr 770	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
79		simpr 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80		simp2 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
81		zssre 10968	. . . . . . . . . . . . . . . . . . . . 21
82		ressxr 9702	. . . . . . . . . . . . . . . . . . . . 21
83	81, 82	sstri 3427	. . . . . . . . . . . . . . . . . . . 20
84		nnnegz 10964	. . . . . . . . . . . . . . . . . . . 20
85	83, 84	sseldi 3416	. . . . . . . . . . . . . . . . . . 19
86	85	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
87	80, 86	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
88	76	nnxrd 37426	. . . . . . . . . . . . . . . . . . 19
89	88	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
90	80, 89	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
91	34	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
92	82	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
93	91, 92	fssd 5750	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
94	93	3adant1l 1284	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95	94	ffvelrnda 6037	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
96		nnre 10638	. . . . . . . . . . . . . . . . . . . . 21
97	96	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
98	97	3ad2antl2 1193	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
99	98	renegcld 10067	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
100	35	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	100	3ad2antl1 1192	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
102	101	renegcld 10067	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
103		simpll 768	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
104		simplr 770	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
105		n0i 3727	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
107	103, 104, 106, 69	syl21anc 1291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
108	107	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
109	34	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
110	36, 109	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
111	110	abscld 13575	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
112	111	adantll 728	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113	112	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
114	109	renegcld 10067	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
115	114	leabsd 13553	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	110	absnegd 13588	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
117	115, 116	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
118	117	adantll 728	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
120	29	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
121	106, 66	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
122	121	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
123		fimaxre2 10574	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
124	29, 44, 123	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
125	124	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
126	125	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
127		elmapfun 7513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128	127	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
129		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
130	56	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
131	130	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
132	129, 131	eleqtrd 2551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
133		fvco 5956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
134	128, 132, 133	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
135	134	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
136		absfun 37660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
137	136	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138		funco 5627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
139	137, 127, 138	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140	139	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
141	110, 49	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
142		dmfco 5954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
143	128, 132, 142	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
144	141, 143	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
145		fvelrn 6030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
146	140, 144, 145	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
147	135, 146	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
148	147	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	148	3ad2antl1 1192	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
150		suprub 10592	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
151	120, 122, 126, 149, 150	syl31anc 1295	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
152	102, 113, 108, 119, 151	letrd 9809	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
153		simpl3 1035	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
154	102, 108, 98, 152, 153	lelttrd 9810	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	102, 98	ltnegd 10212	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
156	154, 155	mpbid 215	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
157	36, 101	sseldi 3416	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
158	157	negnegd 9996	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
159	156, 158	breqtrd 4420	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
160	99, 101, 159	ltled 9800	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	101	leabsd 13553	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
162	101, 113, 108, 161, 151	letrd 9809	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
163	101, 108, 98, 162, 153	lelttrd 9810	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
164	87, 90, 95, 160, 163	elicod 11710	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
165	75, 77, 78, 79, 164	syl31anc 1295	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
166	165	adantlllr 37424	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
167		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
168		mptexg 6151	. . . . . . . . . . . . . . . . . . . . . . . . . 26
169	41, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
170	169	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
171		hoicvr.2	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
173	167, 170, 172	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
174	173	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
175	174	3adant3 1050	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . . 23
177		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . . 24
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
179		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
180		opex 4664	. . . . . . . . . . . . . . . . . . . . . . . 24
181	180	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
182	176, 178, 179, 181	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . . 22
183	182	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
184	175, 183	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
185	184	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
186		negex 9893	. . . . . . . . . . . . . . . . . . . . 21
187		vex 3034	. . . . . . . . . . . . . . . . . . . . 21
188	186, 187	op1st 6820	. . . . . . . . . . . . . . . . . . . 20
189	188	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
190	185, 189	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
191	184	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
192	186, 187	op2nd 6821	. . . . . . . . . . . . . . . . . . . 20
193	192	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
194	191, 193	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
195	190, 194	oveq12d 6326	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
196	195	eqcomd 2477	. . . . . . . . . . . . . . . 16 $/\$ $/\$
197	196	3adant1r 1285	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
198	197	ad5ant135 1280	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
199	166, 198	eleqtrd 2551	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
200	81, 84	sseldi 3416	. . . . . . . . . . . . . . . . . . . . 21
201		opelxpi 4871	. . . . . . . . . . . . . . . . . . . . 21 $/\$
202	200, 96, 201	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20
203	202	ad2antlr 741	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
204		eqid 2471	. . . . . . . . . . . . . . . . . . 19
205	203, 204	fmptd 6061	. . . . . . . . . . . . . . . . . 18 $/\$
206	173	feq1d 5724	. . . . . . . . . . . . . . . . . 18 $/\$
207	205, 206	mpbird 240	. . . . . . . . . . . . . . . . 17 $/\$
208	207	ad4ant14 1259	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209	208	ad2antrr 740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
210		simpr 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
211	209, 210	fvovco 37540	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
212	211	eqcomd 2477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
213	199, 212	eleqtrd 2551	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
214	213	ralrimiva 2809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
215	74, 214	jca 541	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
216		vex 3034	. . . . . . . . . . 11
217	216	elixp 7547	. . . . . . . . . 10 $/\$
218	215, 217	sylibr 217	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
219	218	ex 441	. . . . . . . 8 $/\$ $/\$ $/\$
220	219	reximdva 2858	. . . . . . 7 $/\$ $/\$
221	71, 220	mpd 15	. . . . . 6 $/\$ $/\$
222	22, 23, 24, 221	syl21anc 1291	. . . . 5 $/\$ $/\$
223		eliun 4274	. . . . 5
224	222, 223	sylibr 217	. . . 4 $/\$ $/\$
225	224	ralrimiva 2809	. . 3 $/\$
226		dfss3 3408	. . 3
227	225, 226	sylibr 217	. 2 $/\$
228	21, 227	pm2.61dan 808	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

wss 3390

c0 3722

csn 3959

cop 3965

ciun 4269 class class class wbr 4395

cmpt 4454

wor 4759

cxp 4837

cdm 4839

crn 4840

ccom 4843

wfun 5583

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

c1st 6810

c2nd 6811

cmap 7490

cixp 7540

cfn 7587

csup 7972

cc 9555

cr 9556

c1 9558

cxr 9692

clt 9693

cle 9694

cneg 9881

cn 10631

cz 10961

cico 11662

cabs 13374

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-ico 11666 df-seq 12252 df-exp 12311 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376

This theorem is referenced by: hoicvrrex 38496

W3C validator