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 28582

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 19838	. . . . 5 $/\$
3	1, 2	syl5eqel 2525	. . . 4 $/\$
4		istotbnd3 28579	. . . . 5 $/\$
5	4	baib 891	. . . 4
6	3, 5	syl 16	. . 3 $/\$
7		simpllr 753	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4538	. . . . . . . . . 10
9	7, 8	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3572	. . . . . . . . 9
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 750	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3354	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 751	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 19809	. . . . . . . . . . . . . 14
16	15	ad4antr 726	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7609	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 457	. . . . . . . . . . . . . . . 16
19	18	adantl 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3353	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 761	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3552	. . . . . . . . . . . . . . 15
23	21, 22	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2518	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 753	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11024	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 19906	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3567	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3403	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2797	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4183	. . . . . . . . . 10
33	31, 32	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 711	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3388	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 529	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2823	. . . 4 $/\$ $/\$
39	38	ralimdva 2792	. . 3 $/\$
40	6, 39	sylbid 215	. 2 $/\$
41		simpr 458	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11035	. . . . . 6 $/\$ $/\$
43		oveq2 6098	. . . . . . . . . 10
44	43	iuneq2d 4194	. . . . . . . . 9
45	44	sseq2d 3381	. . . . . . . 8
46	45	rexbidv 2734	. . . . . . 7
47	46	rspcv 3066	. . . . . 6
48	42, 47	syl 16	. . . . 5 $/\$ $/\$
49		elfpw 7609	. . . . . . . . . . 11 $/\$
50	49	simprbi 461	. . . . . . . . . 10
51	50	ad2antrl 722	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3434	. . . . . . . . 9
53		ssfi 7529	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 657	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6097	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3548	. . . . . . . . . . . . . . 15
57		incom 3540	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2489	. . . . . . . . . . . . . 14
59		dfin5 3333	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2489	. . . . . . . . . . . . 13
61	60	neeq1d 2619	. . . . . . . . . . . 12
62		rabn0 3654	. . . . . . . . . . . 12
63	61, 62	syl6bb 261	. . . . . . . . . . 11
64	63	elrab 3114	. . . . . . . . . 10 $/\$
65	64	simprbi 461	. . . . . . . . 9
66	65	rgen 2779	. . . . . . . 8
67		eleq1 2501	. . . . . . . . 9
68	67	ac6sfi 7552	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 657	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5560	. . . . . . . . . . . . . 14
71	70	ad2antrl 722	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3403	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 750	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5544	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5556	. . . . . . . . . . . . . . . . . 18
78		elpreima 5820	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 895	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2729	. . . . . . . . . . . . . . 15
82	81	ad2antrl 722	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6097	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5166	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2509	. . . . . . . . . . . . . 14
88	87	ralrab2 3122	. . . . . . . . . . . . 13
89	83, 88	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1163	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 990	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5562	. . . . . . . . . . . . 13
95	93, 94	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5556	. . . . . . . . . . . . . . 15
97	93, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 989	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7529	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7585	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7592	. . . . . . . . . . . . 13
105	103, 104	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7609	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6097	. . . . . . . . . . . . 13
109	108	cbviunv 4206	. . . . . . . . . . . 12
110	3	ad4antr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 19809	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3353	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 10994	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 727	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 19893	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1213	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2797	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4208	. . . . . . . . . . . . . 14
120	118, 119	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4232	. . . . . . . . . . . . . . 15
122		simplrr 755	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4206	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3399	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3552	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2485	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3663	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3374	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 233	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 991	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2619	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5166	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2509	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3069	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad2antrr 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141	140	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142		cnvimass 5186	. . . . . . . . . . . . . . . . . . . . . . . . . 26
143	49	simplbi 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144	143	ad2antrl 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
145	144	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	99, 145	sstrd 3363	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	142, 146	syl5ss 3364	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148	147	sselda 3353	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		simp-4r 761	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	149	rpred 11023	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151		elpreima 5820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
152	151	simplbda 621	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
153	97, 152	sylan 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154		blhalf 19880	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
155	141, 148, 150, 153, 154	syl22anc 1214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		ssrin 3572	. . . . . . . . . . . . . . . . . . . . . . 23
157	155, 156	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	142	sseli 3349	. . . . . . . . . . . . . . . . . . . . . . . . 25
159		ffvelrn 5838	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	93, 158, 159	syl2an 474	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		simp-5r 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	161, 22	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	160, 162	eleqtrrd 2518	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	114	ad4antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	1	blres 19906	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
166	141, 163, 164, 165	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	157, 166	sseqtr4d 3390	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168		fnfvelrn 5837	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
169	97, 158, 168	syl2an 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170		oveq1 6097	. . . . . . . . . . . . . . . . . . . . . . 23
171	170	ssiun2s 4211	. . . . . . . . . . . . . . . . . . . . . 22
172	169, 171	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	167, 172	sstrd 3363	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	adantlr 709	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	174	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	139, 175	syld 44	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	131, 176	pm2.61dne 2686	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	177	ralrimiva 2797	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179		iunss 4208	. . . . . . . . . . . . . . 15
180	178, 179	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	127, 180	eqsstr3d 3388	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	120, 181	eqssd 3370	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	109, 182	syl5eq 2485	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		iuneq1 4181	. . . . . . . . . . . . 13
185	184	eqeq1d 2449	. . . . . . . . . . . 12
186	185	rspcev 3070	. . . . . . . . . . 11 $/\$
187	107, 183, 186	syl2anc 656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	187	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	92, 188	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
190	189	exlimdv 1695	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
191	69, 190	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
192	191	rexlimdvaa 2840	. . . . 5 $/\$ $/\$
193	48, 192	syld 44	. . . 4 $/\$ $/\$
194	193	ralrimdva 2804	. . 3 $/\$
195		istotbnd3 28579	. . . . 5 $/\$
196	195	baib 891	. . . 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 960

wceq 1364

wex 1591

wcel 1761

wne 2604

wral 2713

wrex 2714

crab 2717

cin 3324

wss 3325

c0 3634

cpw 3857

ciun 4168

cxp 4834

ccnv 4835

cdm 4836

crn 4837

cres 4838

cima 4839

wfn 5410

wf 5411

cfv 5415 (class class class)co 6090

cfn 7306

cr 9277

cxr 9413

cdiv 9989

c2 10367

crp 10987

cxmt 17701

cme 17702

cbl 17703

ctotbnd 28574

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-map 7212 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-2 10376 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-psmet 17709 df-xmet 17710 df-met 17711 df-bl 17712 df-totbnd 28576

This theorem is referenced by: sstotbnd 28583 sstotbnd3 28584

W3C validator