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 32064

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 21370	. . . . 5 $/\$
3	1, 2	syl5eqel 2515	. . . 4 $/\$
4		istotbnd3 32061	. . . . 5 $/\$
5	4	baib 912	. . . 4
6	3, 5	syl 17	. . 3 $/\$
7		simpllr 768	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4668	. . . . . . . . . 10
9	7, 8	sylib 200	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3688	. . . . . . . . 9
11	9, 10	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 763	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 765	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 21341	. . . . . . . . . . . . . 14
16	15	ad4antr 737	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7880	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 462	. . . . . . . . . . . . . . . 16
19	18	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 776	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3668	. . . . . . . . . . . . . . 15
23	21, 22	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11344	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 21438	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3683	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3515	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2840	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4313	. . . . . . . . . 10
33	31, 32	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 722	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3500	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 535	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 436	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2897	. . . 4 $/\$ $/\$
39	38	ralimdva 2834	. . 3 $/\$
40	6, 39	sylbid 219	. 2 $/\$
41		simpr 463	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11355	. . . . . 6 $/\$ $/\$
43		oveq2 6311	. . . . . . . . . 10
44	43	iuneq2d 4324	. . . . . . . . 9
45	44	sseq2d 3493	. . . . . . . 8
46	45	rexbidv 2940	. . . . . . 7
47	46	rspcv 3179	. . . . . 6
48	42, 47	syl 17	. . . . 5 $/\$ $/\$
49		elfpw 7880	. . . . . . . . . . 11 $/\$
50	49	simprbi 466	. . . . . . . . . 10
51	50	ad2antrl 733	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3547	. . . . . . . . 9
53		ssfi 7796	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6310	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3664	. . . . . . . . . . . . . . 15
57		incom 3656	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2480	. . . . . . . . . . . . . 14
59		dfin5 3445	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2480	. . . . . . . . . . . . 13
61	60	neeq1d 2702	. . . . . . . . . . . 12
62		rabn0 3783	. . . . . . . . . . . 12
63	61, 62	syl6bb 265	. . . . . . . . . . 11
64	63	elrab 3230	. . . . . . . . . 10 $/\$
65	64	simprbi 466	. . . . . . . . 9
66	65	rgen 2786	. . . . . . . 8
67		eleq1 2495	. . . . . . . . 9
68	67	ac6sfi 7819	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5748	. . . . . . . . . . . . . 14
71	70	ad2antrl 733	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3515	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 763	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5731	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 765	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5744	. . . . . . . . . . . . . . . . . 18
78		elpreima 6015	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 918	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2862	. . . . . . . . . . . . . . 15
82	81	ad2antrl 733	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 236	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 23	. . . . . . . . . . . . . . 15
85		oveq1 6310	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5185	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2505	. . . . . . . . . . . . . 14
88	87	ralrab2 3238	. . . . . . . . . . . . 13
89	83, 88	sylib 200	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1186	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 436	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 1013	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5750	. . . . . . . . . . . . 13
95	93, 94	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5744	. . . . . . . . . . . . . . 15
97	93, 96	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 1012	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7796	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7853	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7861	. . . . . . . . . . . . 13
105	103, 104	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7880	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 669	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6310	. . . . . . . . . . . . 13
109	108	cbviunv 4336	. . . . . . . . . . . 12
110	3	ad4antr 737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 21341	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 11311	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 738	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 21425	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2840	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4338	. . . . . . . . . . . . . 14
120	118, 119	sylibr 216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4362	. . . . . . . . . . . . . . 15
122		simplrr 770	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4336	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3511	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3668	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 200	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2476	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3792	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3486	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 237	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 1014	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2702	. . . . . . . . . . . . . . . . . . . . 21
134		id 23	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5185	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2505	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 322	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3182	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 474	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad5antr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		cnvimass 5205	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	49	simplbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143	142	ad2antrl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
144	143	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	99, 144	sstrd 3475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	141, 145	syl5ss 3476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	146	sselda 3465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148		simp-4r 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	148	rpred 11343	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150		elpreima 6015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
151	150	simplbda 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
152	97, 151	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		blhalf 21412	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154	140, 147, 149, 152, 153	syl22anc 1266	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155		ssrin 3688	. . . . . . . . . . . . . . . . . . . . . . 23
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	141	sseli 3461	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		ffvelrn 6033	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
159	93, 157, 158	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160		simp-5r 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	160, 22	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	159, 161	eleqtrrd 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	114	ad4antlr 738	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	1	blres 21438	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
165	140, 162, 163, 164	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	156, 165	sseqtr4d 3502	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		fnfvelrn 6032	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
168	97, 157, 167	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		oveq1 6310	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	ssiun2s 4341	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172	166, 171	sstrd 3475	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	172	adantlr 720	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	ex 436	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	139, 174	syld 46	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	131, 175	pm2.61dne 2742	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	176	ralrimiva 2840	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		iunss 4338	. . . . . . . . . . . . . . 15
179	177, 178	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	127, 179	eqsstr3d 3500	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	120, 180	eqssd 3482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	109, 181	syl5eq 2476	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183		iuneq1 4311	. . . . . . . . . . . . 13
184	183	eqeq1d 2425	. . . . . . . . . . . 12
185	184	rspcev 3183	. . . . . . . . . . 11 $/\$
186	107, 182, 185	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 436	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	92, 187	syld 46	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	exlimdv 1769	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	69, 189	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191	190	rexlimdvaa 2919	. . . . 5 $/\$ $/\$
192	48, 191	syld 46	. . . 4 $/\$ $/\$
193	192	ralrimdva 2844	. . 3 $/\$
194		istotbnd3 32061	. . . . 5 $/\$
195	194	baib 912	. . . 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 983

wceq 1438

wex 1660

wcel 1869

wne 2619

wral 2776

wrex 2777

crab 2780

cin 3436

wss 3437

c0 3762

cpw 3980

ciun 4297

cxp 4849

ccnv 4850

cdm 4851

crn 4852

cres 4853

cima 4854

wfn 5594

wf 5595

cfv 5599 (class class class)co 6303

cfn 7575

cr 9540

cxr 9676

cdiv 10271

c2 10661

crp 11304

cxmt 18948

cme 18949

cbl 18950

ctotbnd 32056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-oadd 7192 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-2 10670 df-rp 11305 df-xneg 11411 df-xadd 11412 df-xmul 11413 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-totbnd 32058

This theorem is referenced by: sstotbnd 32065 sstotbnd3 32066

W3C validator