blcld - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > blcld		Unicode version

Theorem blcld 18488

Description: A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)

**Hypotheses**
Ref	Expression
mopni.1
blcld.3

**Assertion**
Ref	Expression
blcld	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem blcld Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mopni.1	. . . . . 6
2	1	mopnuni 18424	. . . . 5
3	2	3ad2ant1 978	. . . 4 $/\$ $/\$
4	3	difeq1d 3424	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3435	. . . 4 $/\$ $/\$ $\$
6		simpl3 962	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 960	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 961	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3429	. . . . . . . . 9 $\$
10	9	adantl 453	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 18314	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1184	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3290	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6048	. . . . . . . . . . . . . 14
15	14	breq1d 4182	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3054	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 609	. . . . . . . . . . 11
19	18	con3and 429	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 188	. . . . . . . . 9 $\$
21	20	adantl 453	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9100	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 643	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 224	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 10742	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 10535	. . . . . . . 8
28	7	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9086	. . . . . . . . . . . . . 14
32	31	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 10835	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 10836	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 18400	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 742	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 10797	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 18394	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3493	. . . . . . . . . . . . 13
44	8	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 10780	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 10787	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2436	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 10699	. . . . . . . . . . . . . . . 16
52	30, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4192	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 18381	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1199	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 18401	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3631	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 18487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1191	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3444	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3318	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2465	. . . . . . . . . . . 12
69		sseq1 3329	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 692	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3012	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1182	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 599	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 461	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2790	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2749	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 18425	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 978	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 889	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2479	. 2 $/\$ $/\$ $\$
82	1	mopntop 18423	. . . 4
83	82	3ad2ant1 978	. . 3 $/\$ $/\$
84		ssrab2 3388	. . . . 5
85	16, 84	eqsstri 3338	. . . 4
86	85, 3	syl5sseq 3356	. . 3 $/\$ $/\$
87		eqid 2404	. . . 4
88	87	iscld2 17047	. . 3 $/\$ $\$
89	83, 86, 88	syl2anc 643	. 2 $/\$ $/\$ $\$
90	81, 89	mpbird 224	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

wrex 2667

crab 2670 $\$ cdif 3277

cin 3279

wss 3280

c0 3588

cuni 3975 class class class wbr 4172

crn 4838

cfv 5413 (class class class)co 6040

cr 8945

cc0 8946

cxr 9075

clt 9076

cle 9077

cq 10530

cxne 10663

cxad 10664

cxmt 16641

cbl 16643

cmopn 16646

ctop 16913

ccld 17035

This theorem is referenced by: blcls 18489 lmle 19207 minveclem4 19286 lhop1lem 19850 ftalem3 20810 ubthlem1 22325

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-sup 7404 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-topgen 13622 df-psmet 16649 df-xmet 16650 df-bl 16652 df-mopn 16653 df-top 16918 df-bases 16920 df-topon 16921 df-cld 17038

W3C validator