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 28673

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 19938	. . . . 5 $/\$
3	1, 2	syl5eqel 2527	. . . 4 $/\$
4		istotbnd3 28670	. . . . 5 $/\$
5	4	baib 896	. . . 4
6	3, 5	syl 16	. . 3 $/\$
7		simpllr 758	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
8		sspwb 4541	. . . . . . . . . 10
9	7, 8	sylib 196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
10		ssrin 3575	. . . . . . . . 9
11	9, 10	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
13	11, 12	sseldd 3357	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
14		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		metxmet 19909	. . . . . . . . . . . . . 14
16	15	ad4antr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
17		elfpw 7613	. . . . . . . . . . . . . . . . 17 $/\$
18	17	simplbi 460	. . . . . . . . . . . . . . . 16
19	18	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
20	19	sselda 3356	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		simp-4r 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22		dfss1 3555	. . . . . . . . . . . . . . 15
23	21, 22	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24	20, 23	eleqtrrd 2520	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25		simpllr 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
26	25	rpxrd 11028	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
27	1	blres 20006	. . . . . . . . . . . . 13 $/\$ $/\$
28	16, 24, 26, 27	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
29		inss1 3570	. . . . . . . . . . . 12
30	28, 29	syl6eqss 3406	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
31	30	ralrimiva 2799	. . . . . . . . . 10 $/\$ $/\$ $/\$
32		ss2iun 4186	. . . . . . . . . 10
33	31, 32	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
34	33	adantrr 716	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
35	14, 34	eqsstr3d 3391	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	13, 35	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$
38	37	reximdv2 2825	. . . 4 $/\$ $/\$
39	38	ralimdva 2794	. . 3 $/\$
40	6, 39	sylbid 215	. 2 $/\$
41		simpr 461	. . . . . . 7 $/\$ $/\$
42	41	rphalfcld 11039	. . . . . 6 $/\$ $/\$
43		oveq2 6099	. . . . . . . . . 10
44	43	iuneq2d 4197	. . . . . . . . 9
45	44	sseq2d 3384	. . . . . . . 8
46	45	rexbidv 2736	. . . . . . 7
47	46	rspcv 3069	. . . . . 6
48	42, 47	syl 16	. . . . 5 $/\$ $/\$
49		elfpw 7613	. . . . . . . . . . 11 $/\$
50	49	simprbi 464	. . . . . . . . . 10
51	50	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52		ssrab2 3437	. . . . . . . . 9
53		ssfi 7533	. . . . . . . . 9 $/\$
54	51, 52, 53	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
55		oveq1 6098	. . . . . . . . . . . . . . . 16
56	55	ineq1d 3551	. . . . . . . . . . . . . . 15
57		incom 3543	. . . . . . . . . . . . . . 15
58	56, 57	syl6eq 2491	. . . . . . . . . . . . . 14
59		dfin5 3336	. . . . . . . . . . . . . 14
60	58, 59	syl6eq 2491	. . . . . . . . . . . . 13
61	60	neeq1d 2621	. . . . . . . . . . . 12
62		rabn0 3657	. . . . . . . . . . . 12
63	61, 62	syl6bb 261	. . . . . . . . . . 11
64	63	elrab 3117	. . . . . . . . . 10 $/\$
65	64	simprbi 464	. . . . . . . . 9
66	65	rgen 2781	. . . . . . . 8
67		eleq1 2503	. . . . . . . . 9
68	67	ac6sfi 7556	. . . . . . . 8 $/\$ $/\$
69	54, 66, 68	sylancl 662	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
70		fdm 5563	. . . . . . . . . . . . . 14
71	70	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$
72	71, 52	syl6eqss 3406	. . . . . . . . . . . 12 $/\$ $/\$
73		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$
74	71	feq2d 5547	. . . . . . . . . . . . 13 $/\$ $/\$
75	73, 74	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
76		simprr 756	. . . . . . . . . . . . . 14 $/\$ $/\$
77		ffn 5559	. . . . . . . . . . . . . . . . . 18
78		elpreima 5823	. . . . . . . . . . . . . . . . . 18 $/\$
79	77, 78	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
80	79	baibd 900	. . . . . . . . . . . . . . . 16 $/\$
81	80	ralbidva 2731	. . . . . . . . . . . . . . 15
82	81	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$
83	76, 82	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
84		id 22	. . . . . . . . . . . . . . 15
85		oveq1 6098	. . . . . . . . . . . . . . . 16
86	85	imaeq2d 5169	. . . . . . . . . . . . . . 15
87	84, 86	eleq12d 2511	. . . . . . . . . . . . . 14
88	87	ralrab2 3125	. . . . . . . . . . . . 13
89	83, 88	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
90	72, 75, 89	3jca 1168	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	90	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	51, 91	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr2 995	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		frn 5565	. . . . . . . . . . . . 13
95	93, 94	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		ffn 5559	. . . . . . . . . . . . . . 15
97	93, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	51	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simpr1 994	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ssfi 7533	. . . . . . . . . . . . . . 15 $/\$
101	98, 99, 100	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		fnfi 7589	. . . . . . . . . . . . . 14 $/\$
103	97, 101, 102	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		rnfi 7596	. . . . . . . . . . . . 13
105	103, 104	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		elfpw 7613	. . . . . . . . . . . 12 $/\$
107	95, 105, 106	sylanbrc 664	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		oveq1 6098	. . . . . . . . . . . . 13
109	108	cbviunv 4209	. . . . . . . . . . . 12
110	3	ad4antr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		metxmet 19909	. . . . . . . . . . . . . . . . 17
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	95	sselda 3356	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		rpxr 10998	. . . . . . . . . . . . . . . . 17
115	114	ad4antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		blssm 19993	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	112, 113, 115, 116	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2799	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		iunss 4211	. . . . . . . . . . . . . 14
120	118, 119	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		iunin1 4235	. . . . . . . . . . . . . . 15
122		simplrr 760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	55	cbviunv 4209	. . . . . . . . . . . . . . . . 17
124	122, 123	syl6sseq 3402	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		dfss1 3555	. . . . . . . . . . . . . . . 16
126	124, 125	sylib 196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	121, 126	syl5eq 2487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		0ss 3666	. . . . . . . . . . . . . . . . . . 19
129		sseq1 3377	. . . . . . . . . . . . . . . . . . 19
130	128, 129	mpbiri 233	. . . . . . . . . . . . . . . . . 18
131	130	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		simpr3 996	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	56	neeq1d 2621	. . . . . . . . . . . . . . . . . . . . 21
134		id 22	. . . . . . . . . . . . . . . . . . . . . 22
135	55	imaeq2d 5169	. . . . . . . . . . . . . . . . . . . . . 22
136	134, 135	eleq12d 2511	. . . . . . . . . . . . . . . . . . . . 21
137	133, 136	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
138	137	rspccva 3072	. . . . . . . . . . . . . . . . . . 19 $/\$
139	132, 138	sylan 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	15	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141	140	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142		cnvimass 5189	. . . . . . . . . . . . . . . . . . . . . . . . . 26
143	49	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144	143	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
145	144	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	99, 145	sstrd 3366	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	142, 146	syl5ss 3367	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148	147	sselda 3356	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	149	rpred 11027	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151		elpreima 5823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
152	151	simplbda 624	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
153	97, 152	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154		blhalf 19980	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
155	141, 148, 150, 153, 154	syl22anc 1219	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		ssrin 3575	. . . . . . . . . . . . . . . . . . . . . . 23
157	155, 156	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	142	sseli 3352	. . . . . . . . . . . . . . . . . . . . . . . . 25
159		ffvelrn 5841	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	93, 158, 159	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		simp-5r 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	161, 22	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	160, 162	eleqtrrd 2520	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	114	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	1	blres 20006	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
166	141, 163, 164, 165	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	157, 166	sseqtr4d 3393	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168		fnfvelrn 5840	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
169	97, 158, 168	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170		oveq1 6098	. . . . . . . . . . . . . . . . . . . . . . 23
171	170	ssiun2s 4214	. . . . . . . . . . . . . . . . . . . . . 22
172	169, 171	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173	167, 172	sstrd 3366	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	173	adantlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175	174	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	139, 175	syld 44	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	131, 176	pm2.61dne 2688	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	177	ralrimiva 2799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179		iunss 4211	. . . . . . . . . . . . . . 15
180	178, 179	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	127, 180	eqsstr3d 3391	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	120, 181	eqssd 3373	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	109, 182	syl5eq 2487	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		iuneq1 4184	. . . . . . . . . . . . 13
185	184	eqeq1d 2451	. . . . . . . . . . . 12
186	185	rspcev 3073	. . . . . . . . . . 11 $/\$
187	107, 183, 186	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188	187	ex 434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	92, 188	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
190	189	exlimdv 1690	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
191	69, 190	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
192	191	rexlimdvaa 2842	. . . . 5 $/\$ $/\$
193	48, 192	syld 44	. . . 4 $/\$ $/\$
194	193	ralrimdva 2806	. . 3 $/\$
195		istotbnd3 28670	. . . . 5 $/\$
196	195	baib 896	. . . 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 965

wceq 1369

wex 1586

wcel 1756

wne 2606

wral 2715

wrex 2716

crab 2719

cin 3327

wss 3328

c0 3637

cpw 3860

ciun 4171

cxp 4838

ccnv 4839

cdm 4840

crn 4841

cres 4842

cima 4843

wfn 5413

wf 5414

cfv 5418 (class class class)co 6091

cfn 7310

cr 9281

cxr 9417

cdiv 9993

c2 10371

crp 10991

cxmt 17801

cme 17802

cbl 17803

ctotbnd 28665

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-cnex 9338 ax-resscn 9339 ax-1cn 9340 ax-icn 9341 ax-addcl 9342 ax-addrcl 9343 ax-mulcl 9344 ax-mulrcl 9345 ax-mulcom 9346 ax-addass 9347 ax-mulass 9348 ax-distr 9349 ax-i2m1 9350 ax-1ne0 9351 ax-1rid 9352 ax-rnegex 9353 ax-rrecex 9354 ax-cnre 9355 ax-pre-lttri 9356 ax-pre-lttrn 9357 ax-pre-ltadd 9358 ax-pre-mulgt0 9359

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-nel 2609 df-ral 2720 df-rex 2721 df-reu 2722 df-rmo 2723 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-1o 6920 df-oadd 6924 df-er 7101 df-map 7216 df-en 7311 df-dom 7312 df-sdom 7313 df-fin 7314 df-pnf 9420 df-mnf 9421 df-xr 9422 df-ltxr 9423 df-le 9424 df-sub 9597 df-neg 9598 df-div 9994 df-2 10380 df-rp 10992 df-xneg 11089 df-xadd 11090 df-xmul 11091 df-psmet 17809 df-xmet 17810 df-met 17811 df-bl 17812 df-totbnd 28667

This theorem is referenced by: sstotbnd 28674 sstotbnd3 28675

W3C validator