metdseq0 - Metamath Proof Explorer

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

Theorem metdseq0 20274

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
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 1022	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2		simprl 750	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
3		simprr 751	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
4		metdscn.j	. . . . . . . 8
5	4	mopni2 19912	. . . . . . 7 $/\$ $/\$
6	1, 2, 3, 5	syl3anc 1213	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
7		simprr 751	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		ssrin 3565	. . . . . . . 8
9	7, 8	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		rpgt0 10992	. . . . . . . . . 10
11		0re 9376	. . . . . . . . . . 11
12		rpre 10987	. . . . . . . . . . 11
13		ltnle 9444	. . . . . . . . . . 11 $/\$
14	11, 12, 13	sylancr 658	. . . . . . . . . 10
15	10, 14	mpbid 210	. . . . . . . . 9
16	15	ad2antrl 722	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simpllr 753	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	breq2d 4294	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	1	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simpl2 987	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	ad2antrr 720	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simpl3 988	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
23	22	ad2antrr 720	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		rpxr 10988	. . . . . . . . . . . . 13
25	24	ad2antrl 722	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		metdscn.f	. . . . . . . . . . . . 13
27	26	metdsge 20269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28	19, 21, 23, 25, 27	syl31anc 1216	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	18, 28	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		incom 3533	. . . . . . . . . . 11
31	30	eqeq1i 2442	. . . . . . . . . 10
32	29, 31	syl6bb 261	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	necon3bbid 2634	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	16, 33	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		ssn0 3660	. . . . . . 7 $/\$
36	9, 34, 35	syl2anc 656	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 36	rexlimddv 2837	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	expr 612	. . . 4 $/\$ $/\$ $/\$ $/\$
39	38	ralrimiva 2791	. . 3 $/\$ $/\$ $/\$
40	4	mopntopon 19858	. . . . . . 7 TopOn
41	40	3ad2ant1 1004	. . . . . 6 $/\$ $/\$ TopOn
42	41	adantr 462	. . . . 5 $/\$ $/\$ $/\$ TopOn
43		topontop 18375	. . . . 5 TopOn
44	42, 43	syl 16	. . . 4 $/\$ $/\$ $/\$
45		toponuni 18376	. . . . . 6 TopOn
46	42, 45	syl 16	. . . . 5 $/\$ $/\$ $/\$
47	20, 46	sseqtrd 3382	. . . 4 $/\$ $/\$ $/\$
48	22, 46	eleqtrd 2511	. . . 4 $/\$ $/\$ $/\$
49		eqid 2435	. . . . 5
50	49	elcls 18521	. . . 4 $/\$ $/\$
51	44, 47, 48, 50	syl3anc 1213	. . 3 $/\$ $/\$ $/\$
52	39, 51	mpbird 232	. 2 $/\$ $/\$ $/\$
53		incom 3533	. . . . . . 7
54	26	metdsf 20268	. . . . . . . . . . . 12 $/\$
55	54	ffvelrnda 5833	. . . . . . . . . . 11 $/\$ $/\$
56	55	3impa 1177	. . . . . . . . . 10 $/\$ $/\$
57		elxrge0 11383	. . . . . . . . . . 11 $/\$
58	57	simplbi 457	. . . . . . . . . 10
59	56, 58	syl 16	. . . . . . . . 9 $/\$ $/\$
60		xrleid 11117	. . . . . . . . 9
61	59, 60	syl 16	. . . . . . . 8 $/\$ $/\$
62	26	metdsge 20269	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 62	mpdan 663	. . . . . . . 8 $/\$ $/\$
64	61, 63	mpbid 210	. . . . . . 7 $/\$ $/\$
65	53, 64	syl5eq 2479	. . . . . 6 $/\$ $/\$
66	65	adantr 462	. . . . 5 $/\$ $/\$ $/\$
67	41	ad2antrr 720	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ TopOn
68	67, 43	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpll2 1023	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
70	67, 45	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71	69, 70	sseqtrd 3382	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
72		simplr 749	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73		simpll1 1022	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74		simpll3 1024	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75	59	ad2antrr 720	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	4	blopn 19919	. . . . . . . . 9 $/\$ $/\$
77	73, 74, 75, 76	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
78		simpr 458	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79		xblcntr 19830	. . . . . . . . 9 $/\$ $/\$ $/\$
80	73, 74, 75, 78, 79	syl112anc 1217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	49	clsndisj 18523	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	68, 71, 72, 77, 80, 81	syl32anc 1221	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	82	ex 434	. . . . . 6 $/\$ $/\$ $/\$
84	83	necon2bd 2652	. . . . 5 $/\$ $/\$ $/\$
85	66, 84	mpd 15	. . . 4 $/\$ $/\$ $/\$
86	57	simprbi 461	. . . . . . . 8
87	56, 86	syl 16	. . . . . . 7 $/\$ $/\$
88		0xr 9420	. . . . . . . 8
89		xrleloe 11111	. . . . . . . 8 $/\$ $\/$
90	88, 59, 89	sylancr 658	. . . . . . 7 $/\$ $/\$ $\/$
91	87, 90	mpbid 210	. . . . . 6 $/\$ $/\$ $\/$
92	91	adantr 462	. . . . 5 $/\$ $/\$ $/\$ $\/$
93	92	ord 377	. . . 4 $/\$ $/\$ $/\$
94	85, 93	mpd 15	. . 3 $/\$ $/\$ $/\$
95	94	eqcomd 2440	. 2 $/\$ $/\$ $/\$
96	52, 95	impbida 823	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1364

wcel 1757

wne 2598

wral 2707

wrex 2708

cin 3317

wss 3318

c0 3627

cuni 4081 class class class wbr 4282

cmpt 4340

ccnv 4828

crn 4830

cfv 5408 (class class class)co 6082

csup 7680

cr 9271

cc0 9272

cpnf 9405

cxr 9407

clt 9408

cle 9409

crp 10981

cicc 11293

cxmt 17647

cbl 17649

cmopn 17652

ctop 18342 TopOnctopon 18343

ccl 18466

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 1671 ax-6 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2416 ax-rep 4393 ax-sep 4403 ax-nul 4411 ax-pow 4460 ax-pr 4521 ax-un 6363 ax-cnex 9328 ax-resscn 9329 ax-1cn 9330 ax-icn 9331 ax-addcl 9332 ax-addrcl 9333 ax-mulcl 9334 ax-mulrcl 9335 ax-mulcom 9336 ax-addass 9337 ax-mulass 9338 ax-distr 9339 ax-i2m1 9340 ax-1ne0 9341 ax-1rid 9342 ax-rnegex 9343 ax-rrecex 9344 ax-cnre 9345 ax-pre-lttri 9346 ax-pre-lttrn 9347 ax-pre-ltadd 9348 ax-pre-mulgt0 9349 ax-pre-sup 9350

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 1702 df-eu 2260 df-mo 2261 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-ne 2600 df-nel 2601 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2966 df-sbc 3178 df-csb 3279 df-dif 3321 df-un 3323 df-in 3325 df-ss 3332 df-pss 3334 df-nul 3628 df-if 3782 df-pw 3852 df-sn 3868 df-pr 3870 df-tp 3872 df-op 3874 df-uni 4082 df-int 4119 df-iun 4163 df-iin 4164 df-br 4283 df-opab 4341 df-mpt 4342 df-tr 4376 df-eprel 4621 df-id 4625 df-po 4630 df-so 4631 df-fr 4668 df-we 4670 df-ord 4711 df-on 4712 df-lim 4713 df-suc 4714 df-xp 4835 df-rel 4836 df-cnv 4837 df-co 4838 df-dm 4839 df-rn 4840 df-res 4841 df-ima 4842 df-iota 5371 df-fun 5410 df-fn 5411 df-f 5412 df-f1 5413 df-fo 5414 df-f1o 5415 df-fv 5416 df-riota 6041 df-ov 6085 df-oprab 6086 df-mpt2 6087 df-om 6468 df-1st 6568 df-2nd 6569 df-recs 6820 df-rdg 6854 df-er 7091 df-map 7206 df-en 7301 df-dom 7302 df-sdom 7303 df-sup 7681 df-pnf 9410 df-mnf 9411 df-xr 9412 df-ltxr 9413 df-le 9414 df-sub 9587 df-neg 9588 df-div 9984 df-nn 10313 df-2 10370 df-n0 10570 df-z 10637 df-uz 10852 df-q 10944 df-rp 10982 df-xneg 11079 df-xadd 11080 df-xmul 11081 df-icc 11297 df-topgen 14367 df-psmet 17655 df-xmet 17656 df-bl 17658 df-mopn 17659 df-top 18347 df-bases 18349 df-topon 18350 df-cld 18467 df-ntr 18468 df-cls 18469

This theorem is referenced by: metnrmlem1a 20278 lebnumlem1 20377

W3C validator