blcld - Metamath Proof Explorer

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

Theorem blcld 21520

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 21456	. . . . 5
3	2	3ad2ant1 1029	. . . 4 $/\$ $/\$
4	3	difeq1d 3550	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3561	. . . 4 $/\$ $/\$ $\$
6		simpl3 1013	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 1011	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 1012	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3555	. . . . . . . . 9 $\$
10	9	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 21346	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1268	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3414	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6298	. . . . . . . . . . . . . 14
15	14	breq1d 4412	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3198	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 631	. . . . . . . . . . 11
19	18	con3dimp 443	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 199	. . . . . . . . 9 $\$
21	20	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9701	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 236	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 11493	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1268	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 11269	. . . . . . . 8
28	7	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9686	. . . . . . . . . . . . . 14
32	31	ad2antrl 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 11586	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 11587	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 21432	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 775	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 11548	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 21426	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1272	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3625	. . . . . . . . . . . . 13
44	8	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 11531	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 764	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 11538	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2485	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 11449	. . . . . . . . . . . . . . . 16
52	30, 51	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4423	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 21413	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1283	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2497	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 21433	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3808	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 774	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 21519	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3570	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3442	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2518	. . . . . . . . . . . 12
69		sseq1 3453	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 717	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3150	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1266	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 620	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 477	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2879	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2802	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 21457	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 1029	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 933	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2530	. 2 $/\$ $/\$ $\$
82	1	mopntop 21455	. . . 4
83	82	3ad2ant1 1029	. . 3 $/\$ $/\$
84		ssrab2 3514	. . . . 5
85	16, 84	eqsstri 3462	. . . 4
86	85, 3	syl5sseq 3480	. . 3 $/\$ $/\$
87		eqid 2451	. . . 4
88	87	iscld2 20043	. . 3 $/\$ $\$
89	83, 86, 88	syl2anc 667	. 2 $/\$ $/\$ $\$
90	81, 89	mpbird 236	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wrex 2738

crab 2741 $\$ cdif 3401

cin 3403

wss 3404

c0 3731

cuni 4198 class class class wbr 4402

crn 4835

cfv 5582 (class class class)co 6290

cr 9538

cc0 9539

cxr 9674

clt 9675

cle 9676

cq 11264

cxne 11406

cxad 11407

cxmt 18955

cbl 18957

cmopn 18960

ctop 19917

ccld 20031

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-sup 7956 df-inf 7957 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-topgen 15342 df-psmet 18962 df-xmet 18963 df-bl 18965 df-mopn 18966 df-top 19921 df-bases 19922 df-topon 19923 df-cld 20034

This theorem is referenced by: blcls 21521 lmle 22271 minveclem4 22374 minveclem4OLD 22386 lhop1lem 22965 ftalem3 23999 ubthlem1 26512

W3C validator