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 30475

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 20992	. . . . 5 $/\$
3	1, 2	syl5eqel 2549	. . . 4 $/\$
4		istotbnd3 30472	. . . . 5 $/\$
5	4	baib 903	. . . 4
6	3, 5	syl 16	. . 3 $/\$
7		simpllr 760	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4705	. . . . . . . . . 10
9	7, 8	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3719	. . . . . . . . 9
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3500	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 757	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 20963	. . . . . . . . . . . . . 14
16	15	ad4antr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7840	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 460	. . . . . . . . . . . . . . . 16
19	18	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3499	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3699	. . . . . . . . . . . . . . 15
23	21, 22	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2548	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11282	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 21060	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3714	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3549	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2871	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4348	. . . . . . . . . 10
33	31, 32	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 716	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3534	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2928	. . . 4 $/\$ $/\$
39	38	ralimdva 2865	. . 3 $/\$
40	6, 39	sylbid 215	. 2 $/\$
41		simpr 461	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11293	. . . . . 6 $/\$ $/\$
43		oveq2 6304	. . . . . . . . . 10
44	43	iuneq2d 4359	. . . . . . . . 9
45	44	sseq2d 3527	. . . . . . . 8
46	45	rexbidv 2968	. . . . . . 7
47	46	rspcv 3206	. . . . . 6
48	42, 47	syl 16	. . . . 5 $/\$ $/\$
49		elfpw 7840	. . . . . . . . . . 11 $/\$
50	49	simprbi 464	. . . . . . . . . 10
51	50	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3581	. . . . . . . . 9
53		ssfi 7759	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6303	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3695	. . . . . . . . . . . . . . 15
57		incom 3687	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2514	. . . . . . . . . . . . . 14
59		dfin5 3479	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2514	. . . . . . . . . . . . 13
61	60	neeq1d 2734	. . . . . . . . . . . 12
62		rabn0 3814	. . . . . . . . . . . 12
63	61, 62	syl6bb 261	. . . . . . . . . . 11
64	63	elrab 3257	. . . . . . . . . 10 $/\$
65	64	simprbi 464	. . . . . . . . 9
66	65	rgen 2817	. . . . . . . 8
67		eleq1 2529	. . . . . . . . 9
68	67	ac6sfi 7782	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 662	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5741	. . . . . . . . . . . . . 14
71	70	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3549	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 756	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5724	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 757	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5737	. . . . . . . . . . . . . . . . . 18
78		elpreima 6008	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 909	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2893	. . . . . . . . . . . . . . 15
82	81	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6303	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5347	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2539	. . . . . . . . . . . . . 14
88	87	ralrab2 3265	. . . . . . . . . . . . 13
89	83, 88	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1176	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 1003	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5743	. . . . . . . . . . . . 13
95	93, 94	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5737	. . . . . . . . . . . . . . 15
97	93, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 1002	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7759	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7816	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7823	. . . . . . . . . . . . 13
105	103, 104	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7840	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6303	. . . . . . . . . . . . 13
109	108	cbviunv 4371	. . . . . . . . . . . 12
110	3	ad4antr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 20963	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3499	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 11252	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 21047	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2871	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4373	. . . . . . . . . . . . . 14
120	118, 119	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4397	. . . . . . . . . . . . . . 15
122		simplrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4371	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3545	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3699	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2510	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3823	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3520	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 233	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 1004	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2734	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5347	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2539	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3209	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad5antr 733	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		cnvimass 5367	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	49	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143	142	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
144	143	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	99, 144	sstrd 3509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	141, 145	syl5ss 3510	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	146	sselda 3499	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148		simp-4r 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	148	rpred 11281	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150		elpreima 6008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
151	150	simplbda 624	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
152	97, 151	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		blhalf 21034	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154	140, 147, 149, 152, 153	syl22anc 1229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155		ssrin 3719	. . . . . . . . . . . . . . . . . . . . . . 23
156	154, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	141	sseli 3495	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
159	93, 157, 158	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160		simp-5r 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	160, 22	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	159, 161	eleqtrrd 2548	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	114	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	1	blres 21060	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
165	140, 162, 163, 164	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	156, 165	sseqtr4d 3536	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
168	97, 157, 167	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	ssiun2s 4376	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172	166, 171	sstrd 3509	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	172	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	139, 174	syld 44	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	131, 175	pm2.61dne 2774	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	176	ralrimiva 2871	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		iunss 4373	. . . . . . . . . . . . . . 15
179	177, 178	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	127, 179	eqsstr3d 3534	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	120, 180	eqssd 3516	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	109, 181	syl5eq 2510	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183		iuneq1 4346	. . . . . . . . . . . . 13
184	183	eqeq1d 2459	. . . . . . . . . . . 12
185	184	rspcev 3210	. . . . . . . . . . 11 $/\$
186	107, 182, 185	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	92, 187	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	exlimdv 1725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	69, 189	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191	190	rexlimdvaa 2950	. . . . 5 $/\$ $/\$
192	48, 191	syld 44	. . . 4 $/\$ $/\$
193	192	ralrimdva 2875	. . 3 $/\$
194		istotbnd3 30472	. . . . 5 $/\$
195	194	baib 903	. . . 4
196	3, 195	syl 16	. . 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 369 $/\$ w3a 973

wceq 1395

wex 1613

wcel 1819

wne 2652

wral 2807

wrex 2808

crab 2811

cin 3470

wss 3471

c0 3793

cpw 4015

ciun 4332

cxp 5006

ccnv 5007

cdm 5008

crn 5009

cres 5010

cima 5011

wfn 5589

wf 5590

cfv 5594 (class class class)co 6296

cfn 7535

cr 9508

cxr 9644

cdiv 10227

c2 10606

crp 11245

cxmt 18530

cme 18531

cbl 18532

ctotbnd 30467

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-2 10615 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-totbnd 30469

This theorem is referenced by: sstotbnd 30476 sstotbnd3 30477

W3C validator