metdseq0 - Metamath Proof Explorer

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

Theorem metdseq0 21857

Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.)

**Hypotheses**
Ref	Expression
metdscn.f	inf
metdscn.j

**Assertion**
Ref	Expression
metdseq0	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem metdseq0 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll1 1044	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2		simprl 762	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
3		simprr 764	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
4		metdscn.j	. . . . . . . 8
5	4	mopni2 21494	. . . . . . 7 $/\$ $/\$
6	1, 2, 3, 5	syl3anc 1264	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
7		simprr 764	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		ssrin 3687	. . . . . . . 8
9	7, 8	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		rpgt0 11313	. . . . . . . . . 10
11		0re 9643	. . . . . . . . . . 11
12		rpre 11308	. . . . . . . . . . 11
13		ltnle 9713	. . . . . . . . . . 11 $/\$
14	11, 12, 13	sylancr 667	. . . . . . . . . 10
15	10, 14	mpbid 213	. . . . . . . . 9
16	15	ad2antrl 732	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simpllr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	breq2d 4432	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	1	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simpl2 1009	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	ad2antrr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simpl3 1010	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
23	22	ad2antrr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		rpxr 11309	. . . . . . . . . . . . 13
25	24	ad2antrl 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		metdscn.f	. . . . . . . . . . . . 13 inf
27	26	metdsge 21852	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28	19, 21, 23, 25, 27	syl31anc 1267	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	18, 28	bitr3d 258	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		incom 3655	. . . . . . . . . . 11
31	30	eqeq1i 2429	. . . . . . . . . 10
32	29, 31	syl6bb 264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	necon3bbid 2671	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	16, 33	mpbid 213	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		ssn0 3795	. . . . . . 7 $/\$
36	9, 34, 35	syl2anc 665	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 36	rexlimddv 2921	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	expr 618	. . . 4 $/\$ $/\$ $/\$ $/\$
39	38	ralrimiva 2839	. . 3 $/\$ $/\$ $/\$
40	4	mopntopon 21440	. . . . . . 7 TopOn
41	40	3ad2ant1 1026	. . . . . 6 $/\$ $/\$ TopOn
42	41	adantr 466	. . . . 5 $/\$ $/\$ $/\$ TopOn
43		topontop 19927	. . . . 5 TopOn
44	42, 43	syl 17	. . . 4 $/\$ $/\$ $/\$
45		toponuni 19928	. . . . . 6 TopOn
46	42, 45	syl 17	. . . . 5 $/\$ $/\$ $/\$
47	20, 46	sseqtrd 3500	. . . 4 $/\$ $/\$ $/\$
48	22, 46	eleqtrd 2512	. . . 4 $/\$ $/\$ $/\$
49		eqid 2422	. . . . 5
50	49	elcls 20075	. . . 4 $/\$ $/\$
51	44, 47, 48, 50	syl3anc 1264	. . 3 $/\$ $/\$ $/\$
52	39, 51	mpbird 235	. 2 $/\$ $/\$ $/\$
53		incom 3655	. . . . . . 7
54	26	metdsf 21851	. . . . . . . . . . . 12 $/\$
55	54	ffvelrnda 6033	. . . . . . . . . . 11 $/\$ $/\$
56	55	3impa 1200	. . . . . . . . . 10 $/\$ $/\$
57		elxrge0 11741	. . . . . . . . . . 11 $/\$
58	57	simplbi 461	. . . . . . . . . 10
59	56, 58	syl 17	. . . . . . . . 9 $/\$ $/\$
60		xrleid 11449	. . . . . . . . 9
61	59, 60	syl 17	. . . . . . . 8 $/\$ $/\$
62	26	metdsge 21852	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 62	mpdan 672	. . . . . . . 8 $/\$ $/\$
64	61, 63	mpbid 213	. . . . . . 7 $/\$ $/\$
65	53, 64	syl5eq 2475	. . . . . 6 $/\$ $/\$
66	65	adantr 466	. . . . 5 $/\$ $/\$ $/\$
67	41	ad2antrr 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ TopOn
68	67, 43	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpll2 1045	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
70	67, 45	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71	69, 70	sseqtrd 3500	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
72		simplr 760	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73		simpll1 1044	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74		simpll3 1046	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75	59	ad2antrr 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	4	blopn 21501	. . . . . . . . 9 $/\$ $/\$
77	73, 74, 75, 76	syl3anc 1264	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
78		simpr 462	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79		xblcntr 21412	. . . . . . . . 9 $/\$ $/\$ $/\$
80	73, 74, 75, 78, 79	syl112anc 1268	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	49	clsndisj 20077	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	68, 71, 72, 77, 80, 81	syl32anc 1272	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	82	ex 435	. . . . . 6 $/\$ $/\$ $/\$
84	83	necon2bd 2639	. . . . 5 $/\$ $/\$ $/\$
85	66, 84	mpd 15	. . . 4 $/\$ $/\$ $/\$
86	57	simprbi 465	. . . . . . . 8
87	56, 86	syl 17	. . . . . . 7 $/\$ $/\$
88		0xr 9687	. . . . . . . 8
89		xrleloe 11443	. . . . . . . 8 $/\$ $\/$
90	88, 59, 89	sylancr 667	. . . . . . 7 $/\$ $/\$ $\/$
91	87, 90	mpbid 213	. . . . . 6 $/\$ $/\$ $\/$
92	91	adantr 466	. . . . 5 $/\$ $/\$ $/\$ $\/$
93	92	ord 378	. . . 4 $/\$ $/\$ $/\$
94	85, 93	mpd 15	. . 3 $/\$ $/\$ $/\$
95	94	eqcomd 2430	. 2 $/\$ $/\$ $/\$
96	52, 95	impbida 840	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1868

wne 2618

wral 2775

wrex 2776

cin 3435

wss 3436

c0 3761

cuni 4216 class class class wbr 4420

cmpt 4479

crn 4850

cfv 5597 (class class class)co 6301 infcinf 7957

cr 9538

cc0 9539

cpnf 9672

cxr 9674

clt 9675

cle 9676

crp 11302

cicc 11638

cxmt 18942

cbl 18944

cmopn 18947

ctop 19903 TopOnctopon 19904

ccl 20019

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 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593 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 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-iin 4299 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-riota 6263 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-om 6703 df-1st 6803 df-2nd 6804 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-er 7367 df-map 7478 df-en 7574 df-dom 7575 df-sdom 7576 df-sup 7958 df-inf 7959 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-icc 11642 df-topgen 15329 df-psmet 18949 df-xmet 18950 df-bl 18952 df-mopn 18953 df-top 19907 df-bases 19908 df-topon 19909 df-cld 20020 df-ntr 20021 df-cls 20022

This theorem is referenced by: metnrmlem1a 21861 lebnumlem1 21975

W3C validator