sstotbnd2 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sstotbnd2		Structured version Unicode version

Theorem sstotbnd2 31532

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.)

**Hypothesis**
Ref	Expression
sstotbnd.2

**Assertion**
Ref	Expression
sstotbnd2	$/\$

Distinct variable groups:

Proof of Theorem sstotbnd2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sstotbnd.2	. . . . 5
2		metres2 21156	. . . . 5 $/\$
3	1, 2	syl5eqel 2494	. . . 4 $/\$
4		istotbnd3 31529	. . . . 5 $/\$
5	4	baib 904	. . . 4
6	3, 5	syl 17	. . 3 $/\$
7		simpllr 761	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4639	. . . . . . . . . 10
9	7, 8	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3663	. . . . . . . . 9
11	9, 10	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3442	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 758	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 21127	. . . . . . . . . . . . . 14
16	15	ad4antr 730	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7855	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 458	. . . . . . . . . . . . . . . 16
19	18	adantl 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3441	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 769	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3643	. . . . . . . . . . . . . . 15
23	21, 22	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 761	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11304	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 21224	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3658	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3491	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2817	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4286	. . . . . . . . . 10
33	31, 32	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 715	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3476	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 530	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 432	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2874	. . . 4 $/\$ $/\$
39	38	ralimdva 2811	. . 3 $/\$
40	6, 39	sylbid 215	. 2 $/\$
41		simpr 459	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11315	. . . . . 6 $/\$ $/\$
43		oveq2 6285	. . . . . . . . . 10
44	43	iuneq2d 4297	. . . . . . . . 9
45	44	sseq2d 3469	. . . . . . . 8
46	45	rexbidv 2917	. . . . . . 7
47	46	rspcv 3155	. . . . . 6
48	42, 47	syl 17	. . . . 5 $/\$ $/\$
49		elfpw 7855	. . . . . . . . . . 11 $/\$
50	49	simprbi 462	. . . . . . . . . 10
51	50	ad2antrl 726	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3523	. . . . . . . . 9
53		ssfi 7774	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 660	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6284	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3639	. . . . . . . . . . . . . . 15
57		incom 3631	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2459	. . . . . . . . . . . . . 14
59		dfin5 3421	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2459	. . . . . . . . . . . . 13
61	60	neeq1d 2680	. . . . . . . . . . . 12
62		rabn0 3758	. . . . . . . . . . . 12
63	61, 62	syl6bb 261	. . . . . . . . . . 11
64	63	elrab 3206	. . . . . . . . . 10 $/\$
65	64	simprbi 462	. . . . . . . . 9
66	65	rgen 2763	. . . . . . . 8
67		eleq1 2474	. . . . . . . . 9
68	67	ac6sfi 7797	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 660	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5717	. . . . . . . . . . . . . 14
71	70	ad2antrl 726	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3491	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 756	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5700	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 758	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5713	. . . . . . . . . . . . . . . . . 18
78		elpreima 5984	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 910	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2839	. . . . . . . . . . . . . . 15
82	81	ad2antrl 726	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6284	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5156	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2484	. . . . . . . . . . . . . 14
88	87	ralrab2 3214	. . . . . . . . . . . . 13
89	83, 88	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1177	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 432	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 1004	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5719	. . . . . . . . . . . . 13
95	93, 94	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5713	. . . . . . . . . . . . . . 15
97	93, 96	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 1003	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7774	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7831	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7838	. . . . . . . . . . . . 13
105	103, 104	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7855	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6284	. . . . . . . . . . . . 13
109	108	cbviunv 4309	. . . . . . . . . . . 12
110	3	ad4antr 730	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 21127	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 11271	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 731	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 21211	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2817	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4311	. . . . . . . . . . . . . 14
120	118, 119	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4335	. . . . . . . . . . . . . . 15
122		simplrr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4309	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3643	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2455	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3767	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3462	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 233	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 1005	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2680	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5156	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2484	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 318	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3158	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 469	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		cnvimass 5176	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	49	simplbi 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143	142	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
144	143	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	99, 144	sstrd 3451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	141, 145	syl5ss 3452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	146	sselda 3441	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148		simp-4r 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	148	rpred 11303	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150		elpreima 5984	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
151	150	simplbda 622	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
152	97, 151	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		blhalf 21198	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154	140, 147, 149, 152, 153	syl22anc 1231	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155		ssrin 3663	. . . . . . . . . . . . . . . . . . . . . . 23
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	141	sseli 3437	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		ffvelrn 6006	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
159	93, 157, 158	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160		simp-5r 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	160, 22	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	159, 161	eleqtrrd 2493	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	114	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	1	blres 21224	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
165	140, 162, 163, 164	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	156, 165	sseqtr4d 3478	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		fnfvelrn 6005	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
168	97, 157, 167	syl2an 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	ssiun2s 4314	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172	166, 171	sstrd 3451	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	172	adantlr 713	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	ex 432	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	139, 174	syld 42	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	131, 175	pm2.61dne 2720	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	176	ralrimiva 2817	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		iunss 4311	. . . . . . . . . . . . . . 15
179	177, 178	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	127, 179	eqsstr3d 3476	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	120, 180	eqssd 3458	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	109, 181	syl5eq 2455	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183		iuneq1 4284	. . . . . . . . . . . . 13
184	183	eqeq1d 2404	. . . . . . . . . . . 12
185	184	rspcev 3159	. . . . . . . . . . 11 $/\$
186	107, 182, 185	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 432	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	92, 187	syld 42	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	exlimdv 1745	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	69, 189	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191	190	rexlimdvaa 2896	. . . . 5 $/\$ $/\$
192	48, 191	syld 42	. . . 4 $/\$ $/\$
193	192	ralrimdva 2821	. . 3 $/\$
194		istotbnd3 31529	. . . . 5 $/\$
195	194	baib 904	. . . 4
196	3, 195	syl 17	. . 3 $/\$
197	193, 196	sylibrd 234	. 2 $/\$
198	40, 197	impbid 191	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wex 1633

wcel 1842

wne 2598

wral 2753

wrex 2754

crab 2757

cin 3412

wss 3413

c0 3737

cpw 3954

ciun 4270

cxp 4820

ccnv 4821

cdm 4822

crn 4823

cres 4824

cima 4825

wfn 5563

wf 5564

cfv 5568 (class class class)co 6277

cfn 7553

cr 9520

cxr 9656

cdiv 10246

c2 10625

crp 11264

cxmt 18721

cme 18722

cbl 18723

ctotbnd 31524

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6683 df-1st 6783 df-2nd 6784 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-1o 7166 df-oadd 7170 df-er 7347 df-map 7458 df-en 7554 df-dom 7555 df-sdom 7556 df-fin 7557 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-div 10247 df-2 10634 df-rp 11265 df-xneg 11370 df-xadd 11371 df-xmul 11372 df-psmet 18729 df-xmet 18730 df-met 18731 df-bl 18732 df-totbnd 31526

This theorem is referenced by: sstotbnd 31533 sstotbnd3 31534

W3C validator