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 38370

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 9630	. . . . . . 7
2		mapdm0 37471	. . . . . . 7
3	1, 2	ax-mp 5	. . . . . 6
4	3	a1i 11	. . . . 5
5		oveq2 6298	. . . . 5
6		ixpeq1 7533	. . . . . . 7
7	6	iuneq2d 4305	. . . . . 6
8		ixp0x 7550	. . . . . . . . . 10
9	8	a1i 11	. . . . . . . . 9
10	9	iuneq2i 4297	. . . . . . . 8
11		1nn 10620	. . . . . . . . . 10
12	11	ne0ii 3738	. . . . . . . . 9
13		iunconst 4287	. . . . . . . . 9
14	12, 13	ax-mp 5	. . . . . . . 8
15	10, 14	eqtri 2473	. . . . . . 7
16	15	a1i 11	. . . . . 6
17	7, 16	eqtrd 2485	. . . . 5
18	4, 5, 17	3eqtr4d 2495	. . . 4
19		eqimss 3484	. . . 4
20	18, 19	syl 17	. . 3
21	20	adantl 468	. 2 $/\$
22		simpll 760	. . . . . 6 $/\$ $/\$
23		simpr 463	. . . . . 6 $/\$ $/\$
24		simplr 762	. . . . . 6 $/\$ $/\$
25		rncoss 5095	. . . . . . . . . . 11
26		absf 13400	. . . . . . . . . . . 12
27		frn 5735	. . . . . . . . . . . 12
28	26, 27	ax-mp 5	. . . . . . . . . . 11
29	25, 28	sstri 3441	. . . . . . . . . 10
30	29	a1i 11	. . . . . . . . 9 $/\$ $/\$
31		ltso 9714	. . . . . . . . . . 11
32	31	a1i 11	. . . . . . . . . 10 $/\$ $/\$
33	26	a1i 11	. . . . . . . . . . . . 13 $/\$
34		elmapi 7493	. . . . . . . . . . . . . . 15
35	34	adantl 468	. . . . . . . . . . . . . 14 $/\$
36		ax-resscn 9596	. . . . . . . . . . . . . . 15
37	36	a1i 11	. . . . . . . . . . . . . 14 $/\$
38	35, 37	fssd 5738	. . . . . . . . . . . . 13 $/\$
39		fco 5739	. . . . . . . . . . . . 13 $/\$
40	33, 38, 39	syl2anc 667	. . . . . . . . . . . 12 $/\$
41		hoicvr.3	. . . . . . . . . . . . 13
42	41	adantr 467	. . . . . . . . . . . 12 $/\$
43		rnffi 37440	. . . . . . . . . . . 12 $/\$
44	40, 42, 43	syl2anc 667	. . . . . . . . . . 11 $/\$
45	44	adantr 467	. . . . . . . . . 10 $/\$ $/\$
46		frn 5735	. . . . . . . . . . . . . . . . . . . 20
47	34, 46	syl 17	. . . . . . . . . . . . . . . . . . 19
48	26	fdmi 5734	. . . . . . . . . . . . . . . . . . . . . 22
49	48	eqcomi 2460	. . . . . . . . . . . . . . . . . . . . 21
50	36, 49	sseqtri 3464	. . . . . . . . . . . . . . . . . . . 20
51	50	a1i 11	. . . . . . . . . . . . . . . . . . 19
52	47, 51	sstrd 3442	. . . . . . . . . . . . . . . . . 18
53		dmcosseq 5096	. . . . . . . . . . . . . . . . . 18
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17
55		fdm 5733	. . . . . . . . . . . . . . . . . 18
56	34, 55	syl 17	. . . . . . . . . . . . . . . . 17
57	54, 56	eqtrd 2485	. . . . . . . . . . . . . . . 16
58	57	adantr 467	. . . . . . . . . . . . . . 15 $/\$
59		neqne 37374	. . . . . . . . . . . . . . . 16
60	59	adantl 468	. . . . . . . . . . . . . . 15 $/\$
61	58, 60	eqnetrd 2691	. . . . . . . . . . . . . 14 $/\$
62	61	neneqd 2629	. . . . . . . . . . . . 13 $/\$
63		dm0rn0 5051	. . . . . . . . . . . . 13
64	62, 63	sylnib 306	. . . . . . . . . . . 12 $/\$
65	64	neqned 2631	. . . . . . . . . . 11 $/\$
66	65	adantll 720	. . . . . . . . . 10 $/\$ $/\$
67		fisupcl 7985	. . . . . . . . . 10 $/\$ $/\$ $/\$
68	32, 45, 66, 30, 67	syl13anc 1270	. . . . . . . . 9 $/\$ $/\$
69	30, 68	sseldd 3433	. . . . . . . 8 $/\$ $/\$
70		arch 10866	. . . . . . . 8
71	69, 70	syl 17	. . . . . . 7 $/\$ $/\$
72	35	ffnd 5729	. . . . . . . . . . . . 13 $/\$
73	72	ad2antrr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
74	73	adantlr 721	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
75		simplll 768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
76		id 22	. . . . . . . . . . . . . . . . 17
77	76	ad3antlr 737	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
78		simplr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
79		simpr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80		simp2 1009	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
81		zssre 10944	. . . . . . . . . . . . . . . . . . . . 21
82		ressxr 9684	. . . . . . . . . . . . . . . . . . . . 21
83	81, 82	sstri 3441	. . . . . . . . . . . . . . . . . . . 20
84		nnnegz 10940	. . . . . . . . . . . . . . . . . . . 20
85	83, 84	sseldi 3430	. . . . . . . . . . . . . . . . . . 19
86	85	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
87	80, 86	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
88	76	nnxrd 37363	. . . . . . . . . . . . . . . . . . 19
89	88	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
90	80, 89	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
91	34	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
92	82	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
93	91, 92	fssd 5738	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
94	93	3adant1l 1260	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95	94	ffvelrnda 6022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
96		nnre 10616	. . . . . . . . . . . . . . . . . . . . 21
97	96	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
98	97	3ad2antl2 1171	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
99	98	renegcld 10046	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
100	35	ffvelrnda 6022	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	100	3ad2antl1 1170	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
102	101	renegcld 10046	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
103		simpll 760	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
104		simplr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
105		n0i 3736	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
107	103, 104, 106, 69	syl21anc 1267	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
108	107	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
109	34	ffvelrnda 6022	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
110	36, 109	sseldi 3430	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
111	110	abscld 13498	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
112	111	adantll 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113	112	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
114	109	renegcld 10046	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
115	114	leabsd 13476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	110	absnegd 13511	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
117	115, 116	breqtrd 4427	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
118	117	adantll 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
120	29	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
121	106, 66	syldan 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
122	121	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
123		fimaxre2 10552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
124	29, 44, 123	sylancr 669	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
125	124	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
126	125	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
127		elmapfun 7495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128	127	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
129		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
130	56	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
131	130	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
132	129, 131	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
133		fvco 5941	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
134	128, 132, 133	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
135	134	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
136		absfun 37573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
137	136	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138		funco 5620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
139	137, 127, 138	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140	139	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
141	110, 49	syl6eleq 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
142		dmfco 5939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
143	128, 132, 142	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
144	141, 143	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
145		fvelrn 6015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
146	140, 144, 145	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
147	135, 146	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
148	147	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	148	3ad2antl1 1170	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
150		suprub 10570	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
151	120, 122, 126, 149, 150	syl31anc 1271	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
152	102, 113, 108, 119, 151	letrd 9792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
153		simpl3 1013	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
154	102, 108, 98, 152, 153	lelttrd 9793	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	102, 98	ltnegd 10191	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
156	154, 155	mpbid 214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
157	36, 101	sseldi 3430	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
158	157	negnegd 9977	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
159	156, 158	breqtrd 4427	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
160	99, 101, 159	ltled 9783	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
161	101	leabsd 13476	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
162	101, 113, 108, 161, 151	letrd 9792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
163	101, 108, 98, 162, 153	lelttrd 9793	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
164	87, 90, 95, 160, 163	elicod 11685	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
165	75, 77, 78, 79, 164	syl31anc 1271	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
166	165	adantlllr 37361	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
167		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
168		mptexg 6135	. . . . . . . . . . . . . . . . . . . . . . . . . 26
169	41, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
170	169	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
171		hoicvr.2	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	fvmpt2 5957	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
173	167, 170, 172	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
174	173	fveq1d 5867	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
175	174	3adant3 1028	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176		eqidd 2452	. . . . . . . . . . . . . . . . . . . . . . 23
177		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . 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 5954	. . . . . . . . . . . . . . . . . . . . . 22
183	182	3ad2ant3 1031	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
184	175, 183	eqtrd 2485	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
185	184	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
186		negex 9873	. . . . . . . . . . . . . . . . . . . . 21
187		vex 3048	. . . . . . . . . . . . . . . . . . . . 21
188	186, 187	op1st 6801	. . . . . . . . . . . . . . . . . . . 20
189	188	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
190	185, 189	eqtrd 2485	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
191	184	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
192	186, 187	op2nd 6802	. . . . . . . . . . . . . . . . . . . 20
193	192	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
194	191, 193	eqtrd 2485	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
195	190, 194	oveq12d 6308	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
196	195	eqcomd 2457	. . . . . . . . . . . . . . . 16 $/\$ $/\$
197	196	3adant1r 1261	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
198	197	ad5ant135 1256	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
199	166, 198	eleqtrd 2531	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
200	81, 84	sseldi 3430	. . . . . . . . . . . . . . . . . . . . 21
201		opelxpi 4866	. . . . . . . . . . . . . . . . . . . . 21 $/\$
202	200, 96, 201	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20
203	202	ad2antlr 733	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
204		eqid 2451	. . . . . . . . . . . . . . . . . . 19
205	203, 204	fmptd 6046	. . . . . . . . . . . . . . . . . 18 $/\$
206	173	feq1d 5714	. . . . . . . . . . . . . . . . . 18 $/\$
207	205, 206	mpbird 236	. . . . . . . . . . . . . . . . 17 $/\$
208	207	ad4ant14 1235	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209	208	ad2antrr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
210		simpr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
211	209, 210	fvovco 37469	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
212	211	eqcomd 2457	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
213	199, 212	eleqtrd 2531	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
214	213	ralrimiva 2802	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
215	74, 214	jca 535	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
216		vex 3048	. . . . . . . . . . 11
217	216	elixp 7529	. . . . . . . . . 10 $/\$
218	215, 217	sylibr 216	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
219	218	ex 436	. . . . . . . 8 $/\$ $/\$ $/\$
220	219	reximdva 2862	. . . . . . 7 $/\$ $/\$
221	71, 220	mpd 15	. . . . . 6 $/\$ $/\$
222	22, 23, 24, 221	syl21anc 1267	. . . . 5 $/\$ $/\$
223		eliun 4283	. . . . 5
224	222, 223	sylibr 216	. . . 4 $/\$ $/\$
225	224	ralrimiva 2802	. . 3 $/\$
226		dfss3 3422	. . 3
227	225, 226	sylibr 216	. 2 $/\$
228	21, 227	pm2.61dan 800	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wne 2622

wral 2737

wrex 2738

cvv 3045

wss 3404

c0 3731

csn 3968

cop 3974

ciun 4278 class class class wbr 4402

cmpt 4461

wor 4754

cxp 4832

cdm 4834

crn 4835

ccom 4838

wfun 5576

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

c1st 6791

c2nd 6792

cmap 7472

cixp 7522

cfn 7569

csup 7954

cc 9537

cr 9538

c1 9540

cxr 9674

clt 9675

cle 9676

cneg 9861

cn 10609

cz 10937

cico 11637

cabs 13297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-map 7474 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-ico 11641 df-seq 12214 df-exp 12273 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299

This theorem is referenced by: hoicvrrex 38378

W3C validator