blcld - Metamath Proof Explorer

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

Theorem blcld 21451

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 21387	. . . . 5
3	2	3ad2ant1 1026	. . . 4 $/\$ $/\$
4	3	difeq1d 3588	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3599	. . . 4 $/\$ $/\$ $\$
6		simpl3 1010	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 1008	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 1009	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3593	. . . . . . . . 9 $\$
10	9	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 21277	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3452	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6313	. . . . . . . . . . . . . 14
15	14	breq1d 4436	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3237	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 629	. . . . . . . . . . 11
19	18	con3dimp 442	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 198	. . . . . . . . 9 $\$
21	20	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9700	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 235	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 11493	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1264	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 11269	. . . . . . . 8
28	7	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9685	. . . . . . . . . . . . . 14
32	31	ad2antrl 732	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 11586	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 11587	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 21363	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 11548	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 213	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 21357	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3661	. . . . . . . . . . . . 13
44	8	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 11531	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 11538	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 11449	. . . . . . . . . . . . . . . 16
52	30, 51	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4446	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 21344	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1279	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 21364	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3842	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 213	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 772	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 21450	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1271	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3608	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3480	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2502	. . . . . . . . . . . 12
69		sseq1 3491	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 715	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3188	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1262	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 618	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 476	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2924	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2846	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 21388	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 1026	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 930	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2518	. 2 $/\$ $/\$ $\$
82	1	mopntop 21386	. . . 4
83	82	3ad2ant1 1026	. . 3 $/\$ $/\$
84		ssrab2 3552	. . . . 5
85	16, 84	eqsstri 3500	. . . 4
86	85, 3	syl5sseq 3518	. . 3 $/\$ $/\$
87		eqid 2429	. . . 4
88	87	iscld2 19974	. . 3 $/\$ $\$
89	83, 86, 88	syl2anc 665	. 2 $/\$ $/\$ $\$
90	81, 89	mpbird 235	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1870

wral 2782

wrex 2783

crab 2786 $\$ cdif 3439

cin 3441

wss 3442

c0 3767

cuni 4222 class class class wbr 4426

crn 4855

cfv 5601 (class class class)co 6305

cr 9537

cc0 9538

cxr 9673

clt 9674

cle 9675

cq 11264

cxne 11406

cxad 11407

cxmt 18890

cbl 18892

cmopn 18895

ctop 19848

ccld 19962

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616

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 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-er 7371 df-map 7482 df-en 7578 df-dom 7579 df-sdom 7580 df-sup 7962 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 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 15301 df-psmet 18897 df-xmet 18898 df-bl 18900 df-mopn 18901 df-top 19852 df-bases 19853 df-topon 19854 df-cld 19965

This theorem is referenced by: blcls 21452 lmle 22164 minveclem4 22267 lhop1lem 22842 ftalem3 23864 ubthlem1 26357

W3C validator