blcld - Metamath Proof Explorer

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

Theorem blcld 20759

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 20695	. . . . 5
3	2	3ad2ant1 1017	. . . 4 $/\$ $/\$
4	3	difeq1d 3621	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3632	. . . 4 $/\$ $/\$ $\$
6		simpl3 1001	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 999	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 1000	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3626	. . . . . . . . 9 $\$
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 20585	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3486	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6291	. . . . . . . . . . . . . 14
15	14	breq1d 4457	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3263	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 625	. . . . . . . . . . 11
19	18	con3dimp 441	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 195	. . . . . . . . 9 $\$
21	20	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9652	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 11398	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1228	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 11186	. . . . . . . 8
28	7	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9638	. . . . . . . . . . . . . 14
32	31	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 11491	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 11492	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 20671	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 11453	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 20665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1232	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3691	. . . . . . . . . . . . 13
44	8	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 11436	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 755	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 11443	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2508	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 11355	. . . . . . . . . . . . . . . 16
52	30, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 20652	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1243	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2520	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 20672	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3870	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 20758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1235	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3641	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3514	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2540	. . . . . . . . . . . 12
69		sseq1 3525	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 710	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3214	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 615	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 474	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2955	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2878	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 20696	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 1017	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 920	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2556	. 2 $/\$ $/\$ $\$
82	1	mopntop 20694	. . . 4
83	82	3ad2ant1 1017	. . 3 $/\$ $/\$
84		ssrab2 3585	. . . . 5
85	16, 84	eqsstri 3534	. . . 4
86	85, 3	syl5sseq 3552	. . 3 $/\$ $/\$
87		eqid 2467	. . . 4
88	87	iscld2 19311	. . 3 $/\$ $\$
89	83, 86, 88	syl2anc 661	. 2 $/\$ $/\$ $\$
90	81, 89	mpbird 232	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wral 2814

wrex 2815

crab 2818 $\$ cdif 3473

cin 3475

wss 3476

c0 3785

cuni 4245 class class class wbr 4447

crn 5000

cfv 5587 (class class class)co 6283

cr 9490

cc0 9491

cxr 9626

clt 9627

cle 9628

cq 11181

cxne 11314

cxad 11315

cxmt 18190

cbl 18192

cmopn 18195

ctop 19177

ccld 19299

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 6575 ax-cnex 9547 ax-resscn 9548 ax-1cn 9549 ax-icn 9550 ax-addcl 9551 ax-addrcl 9552 ax-mulcl 9553 ax-mulrcl 9554 ax-mulcom 9555 ax-addass 9556 ax-mulass 9557 ax-distr 9558 ax-i2m1 9559 ax-1ne0 9560 ax-1rid 9561 ax-rnegex 9562 ax-rrecex 9563 ax-cnre 9564 ax-pre-lttri 9565 ax-pre-lttrn 9566 ax-pre-ltadd 9567 ax-pre-mulgt0 9568 ax-pre-sup 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-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 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288 df-om 6680 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-sup 7900 df-pnf 9629 df-mnf 9630 df-xr 9631 df-ltxr 9632 df-le 9633 df-sub 9806 df-neg 9807 df-div 10206 df-nn 10536 df-2 10593 df-n0 10795 df-z 10864 df-uz 11082 df-q 11182 df-rp 11220 df-xneg 11317 df-xadd 11318 df-xmul 11319 df-topgen 14698 df-psmet 18198 df-xmet 18199 df-bl 18201 df-mopn 18202 df-top 19182 df-bases 19184 df-topon 19185 df-cld 19302

This theorem is referenced by: blcls 20760 lmle 21491 minveclem4 21598 lhop1lem 22165 ftalem3 23092 ubthlem1 25478

W3C validator