metdseq0 - Metamath Proof Explorer

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

Theorem metdseq0 21949

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 1069	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2		simprl 772	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
3		simprr 774	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
4		metdscn.j	. . . . . . . 8
5	4	mopni2 21586	. . . . . . 7 $/\$ $/\$
6	1, 2, 3, 5	syl3anc 1292	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
7		simprr 774	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		ssrin 3648	. . . . . . . 8
9	7, 8	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		rpgt0 11336	. . . . . . . . . 10
11		0re 9661	. . . . . . . . . . 11
12		rpre 11331	. . . . . . . . . . 11
13		ltnle 9731	. . . . . . . . . . 11 $/\$
14	11, 12, 13	sylancr 676	. . . . . . . . . 10
15	10, 14	mpbid 215	. . . . . . . . 9
16	15	ad2antrl 742	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simpllr 777	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	breq2d 4407	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	1	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simpl2 1034	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simpl3 1035	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
23	22	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		rpxr 11332	. . . . . . . . . . . . 13
25	24	ad2antrl 742	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		metdscn.f	. . . . . . . . . . . . 13 inf
27	26	metdsge 21944	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28	19, 21, 23, 25, 27	syl31anc 1295	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	18, 28	bitr3d 263	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		incom 3616	. . . . . . . . . . 11
31	30	eqeq1i 2476	. . . . . . . . . 10
32	29, 31	syl6bb 269	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	necon3bbid 2680	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	16, 33	mpbid 215	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		ssn0 3770	. . . . . . 7 $/\$
36	9, 34, 35	syl2anc 673	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 36	rexlimddv 2875	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	expr 626	. . . 4 $/\$ $/\$ $/\$ $/\$
39	38	ralrimiva 2809	. . 3 $/\$ $/\$ $/\$
40	4	mopntopon 21532	. . . . . . 7 TopOn
41	40	3ad2ant1 1051	. . . . . 6 $/\$ $/\$ TopOn
42	41	adantr 472	. . . . 5 $/\$ $/\$ $/\$ TopOn
43		topontop 20018	. . . . 5 TopOn
44	42, 43	syl 17	. . . 4 $/\$ $/\$ $/\$
45		toponuni 20019	. . . . . 6 TopOn
46	42, 45	syl 17	. . . . 5 $/\$ $/\$ $/\$
47	20, 46	sseqtrd 3454	. . . 4 $/\$ $/\$ $/\$
48	22, 46	eleqtrd 2551	. . . 4 $/\$ $/\$ $/\$
49		eqid 2471	. . . . 5
50	49	elcls 20166	. . . 4 $/\$ $/\$
51	44, 47, 48, 50	syl3anc 1292	. . 3 $/\$ $/\$ $/\$
52	39, 51	mpbird 240	. 2 $/\$ $/\$ $/\$
53		incom 3616	. . . . . . 7
54	26	metdsf 21943	. . . . . . . . . . . 12 $/\$
55	54	ffvelrnda 6037	. . . . . . . . . . 11 $/\$ $/\$
56	55	3impa 1226	. . . . . . . . . 10 $/\$ $/\$
57		elxrge0 11767	. . . . . . . . . . 11 $/\$
58	57	simplbi 467	. . . . . . . . . 10
59	56, 58	syl 17	. . . . . . . . 9 $/\$ $/\$
60		xrleid 11472	. . . . . . . . 9
61	59, 60	syl 17	. . . . . . . 8 $/\$ $/\$
62	26	metdsge 21944	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 62	mpdan 681	. . . . . . . 8 $/\$ $/\$
64	61, 63	mpbid 215	. . . . . . 7 $/\$ $/\$
65	53, 64	syl5eq 2517	. . . . . 6 $/\$ $/\$
66	65	adantr 472	. . . . 5 $/\$ $/\$ $/\$
67	41	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ TopOn
68	67, 43	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpll2 1070	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
70	67, 45	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71	69, 70	sseqtrd 3454	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
72		simplr 770	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73		simpll1 1069	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74		simpll3 1071	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75	59	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	4	blopn 21593	. . . . . . . . 9 $/\$ $/\$
77	73, 74, 75, 76	syl3anc 1292	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
78		simpr 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79		xblcntr 21504	. . . . . . . . 9 $/\$ $/\$ $/\$
80	73, 74, 75, 78, 79	syl112anc 1296	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	49	clsndisj 20168	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	68, 71, 72, 77, 80, 81	syl32anc 1300	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	82	ex 441	. . . . . 6 $/\$ $/\$ $/\$
84	83	necon2bd 2659	. . . . 5 $/\$ $/\$ $/\$
85	66, 84	mpd 15	. . . 4 $/\$ $/\$ $/\$
86	57	simprbi 471	. . . . . . . 8
87	56, 86	syl 17	. . . . . . 7 $/\$ $/\$
88		0xr 9705	. . . . . . . 8
89		xrleloe 11466	. . . . . . . 8 $/\$ $\/$
90	88, 59, 89	sylancr 676	. . . . . . 7 $/\$ $/\$ $\/$
91	87, 90	mpbid 215	. . . . . 6 $/\$ $/\$ $\/$
92	91	adantr 472	. . . . 5 $/\$ $/\$ $/\$ $\/$
93	92	ord 384	. . . 4 $/\$ $/\$ $/\$
94	85, 93	mpd 15	. . 3 $/\$ $/\$ $/\$
95	94	eqcomd 2477	. 2 $/\$ $/\$ $/\$
96	52, 95	impbida 850	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cin 3389

wss 3390

c0 3722

cuni 4190 class class class wbr 4395

cmpt 4454

crn 4840

cfv 5589 (class class class)co 6308 infcinf 7973

cr 9556

cc0 9557

cpnf 9690

cxr 9692

clt 9693

cle 9694

crp 11325

cicc 11663

cxmt 19032

cbl 19034

cmopn 19037

ctop 19994 TopOnctopon 19995

ccl 20110

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-icc 11667 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cld 20111 df-ntr 20112 df-cls 20113

This theorem is referenced by: metnrmlem1a 21953 lebnumlem1 22067

W3C validator