blcld - Metamath Proof Explorer

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

Theorem blcld 20039

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 19975	. . . . 5
3	2	3ad2ant1 1004	. . . 4 $/\$ $/\$
4	3	difeq1d 3470	. . 3 $/\$ $/\$ $\$ $\$
5		difssd 3481	. . . 4 $/\$ $/\$ $\$
6		simpl3 988	. . . . . . 7 $/\$ $/\$ $/\$ $\$
7		simpl1 986	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
8		simpl2 987	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
9		eldifi 3475	. . . . . . . . 9 $\$
10	9	adantl 463	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
11		xmetcl 19865	. . . . . . . 8 $/\$ $/\$
12	7, 8, 10, 11	syl3anc 1213	. . . . . . 7 $/\$ $/\$ $/\$ $\$
13		eldif 3335	. . . . . . . . . 10 $\$ $/\$
14		oveq2 6098	. . . . . . . . . . . . . 14
15	14	breq1d 4299	. . . . . . . . . . . . 13
16		blcld.3	. . . . . . . . . . . . 13
17	15, 16	elrab2 3116	. . . . . . . . . . . 12 $/\$
18	17	simplbi2 622	. . . . . . . . . . 11
19	18	con3and 439	. . . . . . . . . 10 $/\$
20	13, 19	sylbi 195	. . . . . . . . 9 $\$
21	20	adantl 463	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
22		xrltnle 9439	. . . . . . . . 9 $/\$
23	6, 12, 22	syl2anc 656	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
24	21, 23	mpbird 232	. . . . . . 7 $/\$ $/\$ $/\$ $\$
25		qbtwnxr 11166	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 12, 24, 25	syl3anc 1213	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
27		qre 10954	. . . . . . . 8
28	7	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
29	10	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
30	12	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
31		rexr 9425	. . . . . . . . . . . . . 14
32	31	ad2antrl 722	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
33	32	xnegcld 11259	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
34	30, 33	xaddcld 11260	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
35		blelrn 19951	. . . . . . . . . . 11 $/\$ $/\$
36	28, 29, 34, 35	syl3anc 1213	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
37		simprrr 759	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
38		xposdif 11221	. . . . . . . . . . . . 13 $/\$
39	32, 30, 38	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
40	37, 39	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
41		xblcntr 19945	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	28, 29, 34, 40, 41	syl112anc 1217	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
43		incom 3540	. . . . . . . . . . . . 13
44	8	adantr 462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
45		xaddcom 11204	. . . . . . . . . . . . . . . . 17 $/\$
46	32, 34, 45	syl2anc 656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
47		simprl 750	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
48		xnpcan 11211	. . . . . . . . . . . . . . . . 17 $/\$
49	30, 47, 48	syl2anc 656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
50	46, 49	eqtrd 2473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
51		xrleid 11123	. . . . . . . . . . . . . . . 16
52	30, 51	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
53	50, 52	eqbrtrd 4309	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
54		bldisj 19932	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
55	28, 44, 29, 32, 34, 53, 54	syl33anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
56	43, 55	syl5eq 2485	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
57		blssm 19952	. . . . . . . . . . . . . 14 $/\$ $/\$
58	28, 29, 34, 57	syl3anc 1213	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
59		reldisj 3719	. . . . . . . . . . . . 13 $\$
60	58, 59	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
61	56, 60	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
62	6	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
63		simprrl 758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
64	1, 16	blsscls2 20038	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
65	28, 44, 62, 32, 63, 64	syl23anc 1220	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
66	65	sscond 3490	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
67	61, 66	sstrd 3363	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
68		eleq2 2502	. . . . . . . . . . . 12
69		sseq1 3374	. . . . . . . . . . . 12 $\$ $\$
70	68, 69	anbi12d 705	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
71	70	rspcev 3070	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
72	36, 42, 67, 71	syl12anc 1211	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
73	72	expr 612	. . . . . . . 8 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
74	27, 73	sylan2 471	. . . . . . 7 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
75	74	rexlimdva 2839	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$
76	26, 75	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$
77	76	ralrimiva 2797	. . . 4 $/\$ $/\$ $\$ $/\$ $\$
78	1	elmopn 19976	. . . . 5 $\$ $\$ $/\$ $\$ $/\$ $\$
79	78	3ad2ant1 1004	. . . 4 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
80	5, 77, 79	mpbir2and 908	. . 3 $/\$ $/\$ $\$
81	4, 80	eqeltrrd 2516	. 2 $/\$ $/\$ $\$
82	1	mopntop 19974	. . . 4
83	82	3ad2ant1 1004	. . 3 $/\$ $/\$
84		ssrab2 3434	. . . . 5
85	16, 84	eqsstri 3383	. . . 4
86	85, 3	syl5sseq 3401	. . 3 $/\$ $/\$
87		eqid 2441	. . . 4
88	87	iscld2 18591	. . 3 $/\$ $\$
89	83, 86, 88	syl2anc 656	. 2 $/\$ $/\$ $\$
90	81, 89	mpbird 232	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1364

wcel 1761

wral 2713

wrex 2714

crab 2717 $\$ cdif 3322

cin 3324

wss 3325

c0 3634

cuni 4088 class class class wbr 4289

crn 4837

cfv 5415 (class class class)co 6090

cr 9277

cc0 9278

cxr 9413

clt 9414

cle 9415

cq 10949

cxne 11082

cxad 11083

cxmt 17760

cbl 17762

cmopn 17765

ctop 18457

ccld 18579

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-er 7097 df-map 7212 df-en 7307 df-dom 7308 df-sdom 7309 df-sup 7687 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-n0 10576 df-z 10643 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-topgen 14378 df-psmet 17768 df-xmet 17769 df-bl 17771 df-mopn 17772 df-top 18462 df-bases 18464 df-topon 18465 df-cld 18582

This theorem is referenced by: blcls 20040 lmle 20771 minveclem4 20878 lhop1lem 21444 ftalem3 22371 ubthlem1 24206

W3C validator