blcld - Metamath Proof Explorer

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

Theorem blcld 21134

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 21070	. . . . 5
3	2	3ad2ant1 1017	. . . 4 $/\$ $/\$
4	3	difeq1d 3617	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3628	. . . 4 $/\$ $/\$ $\$
6		simpl3 1001	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 999	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 1000	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3622	. . . . . . . . 9 $\$
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 20960	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3481	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6304	. . . . . . . . . . . . . 14
15	14	breq1d 4466	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3259	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 625	. . . . . . . . . . 11
19	18	con3dimp 441	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 195	. . . . . . . . 9 $\$
21	20	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9670	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 11424	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1228	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 11212	. . . . . . . 8
28	7	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9656	. . . . . . . . . . . . . 14
32	31	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 11517	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 11518	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 21046	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 11479	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 21040	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1232	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3687	. . . . . . . . . . . . 13
44	8	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 11462	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 756	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 11469	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2498	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 11381	. . . . . . . . . . . . . . . 16
52	30, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4476	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 21027	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1243	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2510	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 21047	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3873	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 765	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 21133	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1235	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3637	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3509	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2530	. . . . . . . . . . . 12
69		sseq1 3520	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 710	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3210	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 615	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 474	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2949	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2871	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 21071	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 1017	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 922	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2546	. 2 $/\$ $/\$ $\$
82	1	mopntop 21069	. . . 4
83	82	3ad2ant1 1017	. . 3 $/\$ $/\$
84		ssrab2 3581	. . . . 5
85	16, 84	eqsstri 3529	. . . 4
86	85, 3	syl5sseq 3547	. . 3 $/\$ $/\$
87		eqid 2457	. . . 4
88	87	iscld2 19656	. . 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 1395

wcel 1819

wral 2807

wrex 2808

crab 2811 $\$ cdif 3468

cin 3470

wss 3471

c0 3793

cuni 4251 class class class wbr 4456

crn 5009

cfv 5594 (class class class)co 6296

cr 9508

cc0 9509

cxr 9644

clt 9645

cle 9646

cq 11207

cxne 11340

cxad 11341

cxmt 18530

cbl 18532

cmopn 18535

ctop 19521

ccld 19644

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-topgen 14861 df-psmet 18538 df-xmet 18539 df-bl 18541 df-mopn 18542 df-top 19526 df-bases 19528 df-topon 19529 df-cld 19647

This theorem is referenced by: blcls 21135 lmle 21866 minveclem4 21973 lhop1lem 22540 ftalem3 23474 ubthlem1 25913

W3C validator