sstotbnd2 - Mathbox for Jeff Madsen

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

Theorem sstotbnd2 32118

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 21390	. . . . 5 $/\$
3	1, 2	syl5eqel 2535	. . . 4 $/\$
4		istotbnd3 32115	. . . . 5 $/\$
5	4	baib 915	. . . 4
6	3, 5	syl 17	. . 3 $/\$
7		simpllr 770	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4652	. . . . . . . . . 10
9	7, 8	sylib 200	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3659	. . . . . . . . 9
11	9, 10	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 765	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3435	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 767	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 21361	. . . . . . . . . . . . . 14
16	15	ad4antr 739	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7881	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 462	. . . . . . . . . . . . . . . 16
19	18	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3434	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 778	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3639	. . . . . . . . . . . . . . 15
23	21, 22	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2534	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 770	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11349	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 21458	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3654	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3484	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2804	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4297	. . . . . . . . . 10
33	31, 32	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 724	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3469	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 535	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 436	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2860	. . . 4 $/\$ $/\$
39	38	ralimdva 2798	. . 3 $/\$
40	6, 39	sylbid 219	. 2 $/\$
41		simpr 463	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11360	. . . . . 6 $/\$ $/\$
43		oveq2 6303	. . . . . . . . . 10
44	43	iuneq2d 4308	. . . . . . . . 9
45	44	sseq2d 3462	. . . . . . . 8
46	45	rexbidv 2903	. . . . . . 7
47	46	rspcv 3148	. . . . . 6
48	42, 47	syl 17	. . . . 5 $/\$ $/\$
49		elfpw 7881	. . . . . . . . . . 11 $/\$
50	49	simprbi 466	. . . . . . . . . 10
51	50	ad2antrl 735	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3516	. . . . . . . . 9
53		ssfi 7797	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 669	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6302	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3635	. . . . . . . . . . . . . . 15
57		incom 3627	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2503	. . . . . . . . . . . . . 14
59		dfin5 3414	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2503	. . . . . . . . . . . . 13
61	60	neeq1d 2685	. . . . . . . . . . . 12
62		rabn0 3754	. . . . . . . . . . . 12
63	61, 62	syl6bb 265	. . . . . . . . . . 11
64	63	elrab 3198	. . . . . . . . . 10 $/\$
65	64	simprbi 466	. . . . . . . . 9
66	65	rgen 2749	. . . . . . . 8
67		eleq1 2519	. . . . . . . . 9
68	67	ac6sfi 7820	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 669	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5738	. . . . . . . . . . . . . 14
71	70	ad2antrl 735	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3484	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 765	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5720	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 767	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5733	. . . . . . . . . . . . . . . . . 18
78		elpreima 6007	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 921	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2826	. . . . . . . . . . . . . . 15
82	81	ad2antrl 735	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 236	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6302	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5171	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2525	. . . . . . . . . . . . . 14
88	87	ralrab2 3206	. . . . . . . . . . . . 13
89	83, 88	sylib 200	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1189	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 436	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 1016	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5740	. . . . . . . . . . . . 13
95	93, 94	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5733	. . . . . . . . . . . . . . 15
97	93, 96	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 1015	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7797	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7854	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7862	. . . . . . . . . . . . 13
105	103, 104	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7881	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 671	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6302	. . . . . . . . . . . . 13
109	108	cbviunv 4320	. . . . . . . . . . . 12
110	3	ad4antr 739	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 21361	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3434	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 11316	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 21445	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1269	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2804	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4322	. . . . . . . . . . . . . 14
120	118, 119	sylibr 216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4346	. . . . . . . . . . . . . . 15
122		simplrr 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4320	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3639	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 200	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2499	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3765	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3455	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 237	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 1017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2685	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5171	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2525	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 322	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3151	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 474	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad5antr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		cnvimass 5191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	49	simplbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143	142	ad2antrl 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
144	143	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	99, 144	sstrd 3444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	141, 145	syl5ss 3445	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	146	sselda 3434	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148		simp-4r 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	148	rpred 11348	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150		elpreima 6007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
151	150	simplbda 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
152	97, 151	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		blhalf 21432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154	140, 147, 149, 152, 153	syl22anc 1270	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155		ssrin 3659	. . . . . . . . . . . . . . . . . . . . . . 23
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	141	sseli 3430	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		ffvelrn 6025	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
159	93, 157, 158	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160		simp-5r 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	160, 22	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	159, 161	eleqtrrd 2534	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	114	ad4antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	1	blres 21458	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
165	140, 162, 163, 164	syl3anc 1269	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	156, 165	sseqtr4d 3471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		fnfvelrn 6024	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
168	97, 157, 167	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	ssiun2s 4325	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172	166, 171	sstrd 3444	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	172	adantlr 722	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	ex 436	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	139, 174	syld 45	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	131, 175	pm2.61dne 2712	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	176	ralrimiva 2804	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		iunss 4322	. . . . . . . . . . . . . . 15
179	177, 178	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	127, 179	eqsstr3d 3469	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	120, 180	eqssd 3451	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	109, 181	syl5eq 2499	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183		iuneq1 4295	. . . . . . . . . . . . 13
184	183	eqeq1d 2455	. . . . . . . . . . . 12
185	184	rspcev 3152	. . . . . . . . . . 11 $/\$
186	107, 182, 185	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 436	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	92, 187	syld 45	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	exlimdv 1781	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	69, 189	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191	190	rexlimdvaa 2882	. . . . 5 $/\$ $/\$
192	48, 191	syld 45	. . . 4 $/\$ $/\$
193	192	ralrimdva 2808	. . 3 $/\$
194		istotbnd3 32115	. . . . 5 $/\$
195	194	baib 915	. . . 4
196	3, 195	syl 17	. . 3 $/\$
197	193, 196	sylibrd 238	. 2 $/\$
198	40, 197	impbid 194	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1446

wex 1665

wcel 1889

wne 2624

wral 2739

wrex 2740

crab 2743

cin 3405

wss 3406

c0 3733

cpw 3953

ciun 4281

cxp 4835

ccnv 4836

cdm 4837

crn 4838

cres 4839

cima 4840

wfn 5580

wf 5581

cfv 5585 (class class class)co 6295

cfn 7574

cr 9543

cxr 9679

cdiv 10276

c2 10666

crp 11309

cxmt 18967

cme 18968

cbl 18969

ctotbnd 32110

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-2 10675 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-psmet 18974 df-xmet 18975 df-met 18976 df-bl 18977 df-totbnd 32112

This theorem is referenced by: sstotbnd 32119 sstotbnd3 32120

W3C validator