isbnd3 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > isbnd3		Structured version Unicode version

Theorem isbnd3 32023

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.)

**Assertion**
Ref	Expression
isbnd3	$/\$

Distinct variable groups:

Proof of Theorem isbnd3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bndmet 32020	. . 3
2		0re 9594	. . . . . 6
3	2	ne0ii 3711	. . . . 5
4		metf 21287	. . . . . . . . . 10
5		ffn 5689	. . . . . . . . . 10
6	4, 5	syl 17	. . . . . . . . 9
7	1, 6	syl 17	. . . . . . . 8
8	7	ad2antrr 730	. . . . . . 7 $/\$ $/\$
9	1, 4	syl 17	. . . . . . . . . . . 12
10		fdm 5693	. . . . . . . . . . . 12
11	9, 10	syl 17	. . . . . . . . . . 11
12		xpeq2 4811	. . . . . . . . . . . 12
13		xp0 5217	. . . . . . . . . . . 12
14	12, 13	syl6eq 2478	. . . . . . . . . . 11
15	11, 14	sylan9eq 2482	. . . . . . . . . 10 $/\$
16	15	adantr 466	. . . . . . . . 9 $/\$ $/\$
17		dm0rn0 5013	. . . . . . . . 9
18	16, 17	sylib 199	. . . . . . . 8 $/\$ $/\$
19		0ss 3736	. . . . . . . 8
20	18, 19	syl6eqss 3457	. . . . . . 7 $/\$ $/\$
21		df-f 5548	. . . . . . 7 $/\$
22	8, 20, 21	sylanbrc 668	. . . . . 6 $/\$ $/\$
23	22	ralrimiva 2779	. . . . 5 $/\$
24		r19.2z 3831	. . . . 5 $/\$
25	3, 23, 24	sylancr 667	. . . 4 $/\$
26		isbnd2 32022	. . . . . 6 $/\$ $/\$
27	26	simprbi 465	. . . . 5 $/\$
28		2re 10630	. . . . . . . . . . 11
29		simprlr 771	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30	29	rpred 11292	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31		remulcl 9575	. . . . . . . . . . 11 $/\$
32	28, 30, 31	sylancr 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
33	6	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34		simpll 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
35		simprl 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
36		simprr 764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
37		metcl 21289	. . . . . . . . . . . . . 14 $/\$ $/\$
38	34, 35, 36, 37	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
39		metge0 21302	. . . . . . . . . . . . . 14 $/\$ $/\$
40	34, 35, 36, 39	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
41	32	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
42		simprll 770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
43	42	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
44		metcl 21289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
45	34, 43, 35, 44	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
46		metcl 21289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
47	34, 43, 36, 46	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 47	readdcld 9621	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
49		mettri2 21298	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
50	34, 43, 35, 36, 49	syl13anc 1266	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
51	30	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
52		simplrr 769	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
53	35, 52	eleqtrd 2508	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
54		metxmet 21291	. . . . . . . . . . . . . . . . . . . 20
55	34, 54	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
56		rpxr 11260	. . . . . . . . . . . . . . . . . . . . 21
57	56	ad2antlr 731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
58	57	ad2antlr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
59		elbl2 21347	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
60	55, 58, 43, 35, 59	syl22anc 1265	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
61	53, 60	mpbid 213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
62	36, 52	eleqtrd 2508	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
63		elbl2 21347	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
64	55, 58, 43, 36, 63	syl22anc 1265	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
65	62, 64	mpbid 213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
66	45, 47, 51, 51, 61, 65	lt2addd 10187	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
67	51	recnd 9620	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
68	67	2timesd 10806	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
69	66, 68	breqtrrd 4393	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
70	38, 48, 41, 50, 69	lelttrd 9744	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	38, 41, 70	ltled 9734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72		elicc2 11650	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
73	2, 41, 72	sylancr 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	38, 40, 71, 73	mpbir3and 1188	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	ralrimivva 2786	. . . . . . . . . . 11 $/\$ $/\$ $/\$
76		ffnov 6358	. . . . . . . . . . 11 $/\$
77	33, 75, 76	sylanbrc 668	. . . . . . . . . 10 $/\$ $/\$ $/\$
78		oveq2 6257	. . . . . . . . . . . 12
79	78	feq3d 5677	. . . . . . . . . . 11
80	79	rspcev 3125	. . . . . . . . . 10 $/\$
81	32, 77, 80	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	expr 618	. . . . . . . 8 $/\$ $/\$
83	82	rexlimdvva 2863	. . . . . . 7
84	1, 83	syl 17	. . . . . 6
85	84	adantr 466	. . . . 5 $/\$
86	27, 85	mpd 15	. . . 4 $/\$
87	25, 86	pm2.61dane 2688	. . 3
88	1, 87	jca 534	. 2 $/\$
89		simpll 758	. . . 4 $/\$ $/\$
90		simpllr 767	. . . . . . 7 $/\$ $/\$ $/\$
91	89	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$
92		simpr 462	. . . . . . . . 9 $/\$ $/\$ $/\$
93		met0 21300	. . . . . . . . 9 $/\$
94	91, 92, 93	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$
95		simplr 760	. . . . . . . . . . 11 $/\$ $/\$ $/\$
96	95, 92, 92	fovrnd 6399	. . . . . . . . . 10 $/\$ $/\$ $/\$
97		elicc2 11650	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98	2, 90, 97	sylancr 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbid 213	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
100	99	simp3d 1019	. . . . . . . 8 $/\$ $/\$ $/\$
101	94, 100	eqbrtrrd 4389	. . . . . . 7 $/\$ $/\$ $/\$
102	90, 101	ge0p1rpd 11319	. . . . . 6 $/\$ $/\$ $/\$
103		fovrn 6397	. . . . . . . . . . . . . 14 $/\$ $/\$
104	103	3expa 1205	. . . . . . . . . . . . 13 $/\$ $/\$
105	104	adantlll 722	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106		elicc2 11650	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	2, 90, 106	sylancr 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	105, 108	mpbid 213	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	109	simp1d 1017	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
111	90	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
112		peano2re 9757	. . . . . . . . . . . 12
113	90, 112	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
115	109	simp3d 1019	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
116	111	ltp1d 10488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117	110, 111, 114, 115, 116	lelttrd 9744	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
118	117	ralrimiva 2779	. . . . . . . 8 $/\$ $/\$ $/\$
119		rabid2 2945	. . . . . . . 8
120	118, 119	sylibr 215	. . . . . . 7 $/\$ $/\$ $/\$
121	91, 54	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
122	113	rexrd 9641	. . . . . . . 8 $/\$ $/\$ $/\$
123		blval 21343	. . . . . . . 8 $/\$ $/\$
124	121, 92, 122, 123	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$
125	120, 124	eqtr4d 2465	. . . . . 6 $/\$ $/\$ $/\$
126		oveq2 6257	. . . . . . . 8
127	126	eqeq2d 2438	. . . . . . 7
128	127	rspcev 3125	. . . . . 6 $/\$
129	102, 125, 128	syl2anc 665	. . . . 5 $/\$ $/\$ $/\$
130	129	ralrimiva 2779	. . . 4 $/\$ $/\$
131		isbnd 32019	. . . 4 $/\$
132	89, 130, 131	sylanbrc 668	. . 3 $/\$ $/\$
133	132	r19.29an 2908	. 2 $/\$
134	88, 133	impbii 190	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2599

wral 2714

wrex 2715

crab 2718

wss 3379

c0 3704 class class class wbr 4366

cxp 4794

cdm 4796

crn 4797

wfn 5539

wf 5540

cfv 5544 (class class class)co 6249

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

cxr 9625

clt 9626

cle 9627

c2 10610

crp 11253

cicc 11589

cxmt 18898

cme 18899

cbl 18900

cbnd 32006

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-nel 2602 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-op 3948 df-uni 4163 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-id 4711 df-po 4717 df-so 4718 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-riota 6211 df-ov 6252 df-oprab 6253 df-mpt2 6254 df-1st 6751 df-2nd 6752 df-er 7318 df-ec 7320 df-map 7429 df-en 7525 df-dom 7526 df-sdom 7527 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9813 df-neg 9814 df-div 10221 df-2 10619 df-rp 11254 df-xneg 11360 df-xadd 11361 df-xmul 11362 df-icc 11593 df-psmet 18905 df-xmet 18906 df-met 18907 df-bl 18908 df-bnd 32018

This theorem is referenced by: isbnd3b 32024 prdsbnd 32032

W3C validator