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 29901

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 20629	. . . . 5 $/\$
3	1, 2	syl5eqel 2559	. . . 4 $/\$
4		istotbnd3 29898	. . . . 5 $/\$
5	4	baib 901	. . . 4
6	3, 5	syl 16	. . 3 $/\$
7		simpllr 758	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4696	. . . . . . . . . 10
9	7, 8	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3723	. . . . . . . . 9
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3505	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 20600	. . . . . . . . . . . . . 14
16	15	ad4antr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7822	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 460	. . . . . . . . . . . . . . . 16
19	18	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3504	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3703	. . . . . . . . . . . . . . 15
23	21, 22	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2558	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11257	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 20697	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3718	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3554	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2878	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4341	. . . . . . . . . 10
33	31, 32	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 716	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3539	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2934	. . . 4 $/\$ $/\$
39	38	ralimdva 2872	. . 3 $/\$
40	6, 39	sylbid 215	. 2 $/\$
41		simpr 461	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11268	. . . . . 6 $/\$ $/\$
43		oveq2 6292	. . . . . . . . . 10
44	43	iuneq2d 4352	. . . . . . . . 9
45	44	sseq2d 3532	. . . . . . . 8
46	45	rexbidv 2973	. . . . . . 7
47	46	rspcv 3210	. . . . . 6
48	42, 47	syl 16	. . . . 5 $/\$ $/\$
49		elfpw 7822	. . . . . . . . . . 11 $/\$
50	49	simprbi 464	. . . . . . . . . 10
51	50	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3585	. . . . . . . . 9
53		ssfi 7740	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6291	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3699	. . . . . . . . . . . . . . 15
57		incom 3691	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2524	. . . . . . . . . . . . . 14
59		dfin5 3484	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2524	. . . . . . . . . . . . 13
61	60	neeq1d 2744	. . . . . . . . . . . 12
62		rabn0 3805	. . . . . . . . . . . 12
63	61, 62	syl6bb 261	. . . . . . . . . . 11
64	63	elrab 3261	. . . . . . . . . 10 $/\$
65	64	simprbi 464	. . . . . . . . 9
66	65	rgen 2824	. . . . . . . 8
67		eleq1 2539	. . . . . . . . 9
68	67	ac6sfi 7764	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 662	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5735	. . . . . . . . . . . . . 14
71	70	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3554	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5718	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 756	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5731	. . . . . . . . . . . . . . . . . 18
78		elpreima 6001	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 907	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2900	. . . . . . . . . . . . . . 15
82	81	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6291	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5337	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2549	. . . . . . . . . . . . . 14
88	87	ralrab2 3269	. . . . . . . . . . . . 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 5737	. . . . . . . . . . . . 13
95	93, 94	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5731	. . . . . . . . . . . . . . 15
97	93, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 1002	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7740	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7798	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7805	. . . . . . . . . . . . 13
105	103, 104	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7822	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6291	. . . . . . . . . . . . 13
109	108	cbviunv 4364	. . . . . . . . . . . 12
110	3	ad4antr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 20600	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3504	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 11227	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 20684	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2878	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4366	. . . . . . . . . . . . . 14
120	118, 119	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4390	. . . . . . . . . . . . . . 15
122		simplrr 760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4364	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3550	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3703	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2520	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3814	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3525	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 233	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 1004	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2744	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5337	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2549	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3213	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141	140	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142		cnvimass 5357	. . . . . . . . . . . . . . . . . . . . . . . . . 26
143	49	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144	143	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
145	144	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	99, 145	sstrd 3514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	142, 146	syl5ss 3515	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148	147	sselda 3504	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	149	rpred 11256	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151		elpreima 6001	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
152	151	simplbda 624	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
153	97, 152	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154		blhalf 20671	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
155	141, 148, 150, 153, 154	syl22anc 1229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		ssrin 3723	. . . . . . . . . . . . . . . . . . . . . . 23
157	155, 156	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	142	sseli 3500	. . . . . . . . . . . . . . . . . . . . . . . . 25
159		ffvelrn 6019	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	93, 158, 159	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		simp-5r 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	161, 22	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	160, 162	eleqtrrd 2558	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	114	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	1	blres 20697	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
166	141, 163, 164, 165	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	157, 166	sseqtr4d 3541	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168		fnfvelrn 6018	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
169	97, 158, 168	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170		oveq1 6291	. . . . . . . . . . . . . . . . . . . . . . 23
171	170	ssiun2s 4369	. . . . . . . . . . . . . . . . . . . . . 22
172	169, 171	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	167, 172	sstrd 3514	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	174	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	139, 175	syld 44	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	131, 176	pm2.61dne 2784	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	177	ralrimiva 2878	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179		iunss 4366	. . . . . . . . . . . . . . 15
180	178, 179	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	127, 180	eqsstr3d 3539	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	120, 181	eqssd 3521	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	109, 182	syl5eq 2520	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		iuneq1 4339	. . . . . . . . . . . . 13
185	184	eqeq1d 2469	. . . . . . . . . . . 12
186	185	rspcev 3214	. . . . . . . . . . 11 $/\$
187	107, 183, 186	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	187	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	92, 188	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
190	189	exlimdv 1700	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
191	69, 190	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
192	191	rexlimdvaa 2956	. . . . 5 $/\$ $/\$
193	48, 192	syld 44	. . . 4 $/\$ $/\$
194	193	ralrimdva 2882	. . 3 $/\$
195		istotbnd3 29898	. . . . 5 $/\$
196	195	baib 901	. . . 4
197	3, 196	syl 16	. . 3 $/\$
198	194, 197	sylibrd 234	. 2 $/\$
199	40, 198	impbid 191	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

crab 2818

cin 3475

wss 3476

c0 3785

cpw 4010

ciun 4325

cxp 4997

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cfn 7516

cr 9491

cxr 9627

cdiv 10206

c2 10585

crp 11220

cxmt 18202

cme 18203

cbl 18204

ctotbnd 29893

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-2 10594 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-totbnd 29895

This theorem is referenced by: sstotbnd 29902 sstotbnd3 29903

W3C validator