metdseq0 - Metamath Proof Explorer

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

Theorem metdseq0 20433

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 1027	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2		simprl 755	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
3		simprr 756	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
4		metdscn.j	. . . . . . . 8
5	4	mopni2 20071	. . . . . . 7 $/\$ $/\$
6	1, 2, 3, 5	syl3anc 1218	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
7		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		ssrin 3578	. . . . . . . 8
9	7, 8	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		rpgt0 11005	. . . . . . . . . 10
11		0re 9389	. . . . . . . . . . 11
12		rpre 11000	. . . . . . . . . . 11
13		ltnle 9457	. . . . . . . . . . 11 $/\$
14	11, 12, 13	sylancr 663	. . . . . . . . . 10
15	10, 14	mpbid 210	. . . . . . . . 9
16	15	ad2antrl 727	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simpllr 758	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	breq2d 4307	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	1	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simpl2 992	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simpl3 993	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
23	22	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		rpxr 11001	. . . . . . . . . . . . 13
25	24	ad2antrl 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		metdscn.f	. . . . . . . . . . . . 13
27	26	metdsge 20428	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28	19, 21, 23, 25, 27	syl31anc 1221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	18, 28	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		incom 3546	. . . . . . . . . . 11
31	30	eqeq1i 2450	. . . . . . . . . 10
32	29, 31	syl6bb 261	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	necon3bbid 2645	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	16, 33	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		ssn0 3673	. . . . . . 7 $/\$
36	9, 34, 35	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 36	rexlimddv 2848	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	expr 615	. . . 4 $/\$ $/\$ $/\$ $/\$
39	38	ralrimiva 2802	. . 3 $/\$ $/\$ $/\$
40	4	mopntopon 20017	. . . . . . 7 TopOn
41	40	3ad2ant1 1009	. . . . . 6 $/\$ $/\$ TopOn
42	41	adantr 465	. . . . 5 $/\$ $/\$ $/\$ TopOn
43		topontop 18534	. . . . 5 TopOn
44	42, 43	syl 16	. . . 4 $/\$ $/\$ $/\$
45		toponuni 18535	. . . . . 6 TopOn
46	42, 45	syl 16	. . . . 5 $/\$ $/\$ $/\$
47	20, 46	sseqtrd 3395	. . . 4 $/\$ $/\$ $/\$
48	22, 46	eleqtrd 2519	. . . 4 $/\$ $/\$ $/\$
49		eqid 2443	. . . . 5
50	49	elcls 18680	. . . 4 $/\$ $/\$
51	44, 47, 48, 50	syl3anc 1218	. . 3 $/\$ $/\$ $/\$
52	39, 51	mpbird 232	. 2 $/\$ $/\$ $/\$
53		incom 3546	. . . . . . 7
54	26	metdsf 20427	. . . . . . . . . . . 12 $/\$
55	54	ffvelrnda 5846	. . . . . . . . . . 11 $/\$ $/\$
56	55	3impa 1182	. . . . . . . . . 10 $/\$ $/\$
57		elxrge0 11397	. . . . . . . . . . 11 $/\$
58	57	simplbi 460	. . . . . . . . . 10
59	56, 58	syl 16	. . . . . . . . 9 $/\$ $/\$
60		xrleid 11130	. . . . . . . . 9
61	59, 60	syl 16	. . . . . . . 8 $/\$ $/\$
62	26	metdsge 20428	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 62	mpdan 668	. . . . . . . 8 $/\$ $/\$
64	61, 63	mpbid 210	. . . . . . 7 $/\$ $/\$
65	53, 64	syl5eq 2487	. . . . . 6 $/\$ $/\$
66	65	adantr 465	. . . . 5 $/\$ $/\$ $/\$
67	41	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ TopOn
68	67, 43	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpll2 1028	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
70	67, 45	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71	69, 70	sseqtrd 3395	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
72		simplr 754	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73		simpll1 1027	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74		simpll3 1029	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75	59	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	4	blopn 20078	. . . . . . . . 9 $/\$ $/\$
77	73, 74, 75, 76	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
78		simpr 461	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79		xblcntr 19989	. . . . . . . . 9 $/\$ $/\$ $/\$
80	73, 74, 75, 78, 79	syl112anc 1222	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	49	clsndisj 18682	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	68, 71, 72, 77, 80, 81	syl32anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	82	ex 434	. . . . . 6 $/\$ $/\$ $/\$
84	83	necon2bd 2663	. . . . 5 $/\$ $/\$ $/\$
85	66, 84	mpd 15	. . . 4 $/\$ $/\$ $/\$
86	57	simprbi 464	. . . . . . . 8
87	56, 86	syl 16	. . . . . . 7 $/\$ $/\$
88		0xr 9433	. . . . . . . 8
89		xrleloe 11124	. . . . . . . 8 $/\$ $\/$
90	88, 59, 89	sylancr 663	. . . . . . 7 $/\$ $/\$ $\/$
91	87, 90	mpbid 210	. . . . . 6 $/\$ $/\$ $\/$
92	91	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $\/$
93	92	ord 377	. . . 4 $/\$ $/\$ $/\$
94	85, 93	mpd 15	. . 3 $/\$ $/\$ $/\$
95	94	eqcomd 2448	. 2 $/\$ $/\$ $/\$
96	52, 95	impbida 828	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2609

wral 2718

wrex 2719

cin 3330

wss 3331

c0 3640

cuni 4094 class class class wbr 4295

cmpt 4353

ccnv 4842

crn 4844

cfv 5421 (class class class)co 6094

csup 7693

cr 9284

cc0 9285

cpnf 9418

cxr 9420

clt 9421

cle 9422

crp 10994

cicc 11306

cxmt 17804

cbl 17806

cmopn 17809

ctop 18501 TopOnctopon 18502

ccl 18625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4406 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-cnex 9341 ax-resscn 9342 ax-1cn 9343 ax-icn 9344 ax-addcl 9345 ax-addrcl 9346 ax-mulcl 9347 ax-mulrcl 9348 ax-mulcom 9349 ax-addass 9350 ax-mulass 9351 ax-distr 9352 ax-i2m1 9353 ax-1ne0 9354 ax-1rid 9355 ax-rnegex 9356 ax-rrecex 9357 ax-cnre 9358 ax-pre-lttri 9359 ax-pre-lttrn 9360 ax-pre-ltadd 9361 ax-pre-mulgt0 9362 ax-pre-sup 9363

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-int 4132 df-iun 4176 df-iin 4177 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-om 6480 df-1st 6580 df-2nd 6581 df-recs 6835 df-rdg 6869 df-er 7104 df-map 7219 df-en 7314 df-dom 7315 df-sdom 7316 df-sup 7694 df-pnf 9423 df-mnf 9424 df-xr 9425 df-ltxr 9426 df-le 9427 df-sub 9600 df-neg 9601 df-div 9997 df-nn 10326 df-2 10383 df-n0 10583 df-z 10650 df-uz 10865 df-q 10957 df-rp 10995 df-xneg 11092 df-xadd 11093 df-xmul 11094 df-icc 11310 df-topgen 14385 df-psmet 17812 df-xmet 17813 df-bl 17815 df-mopn 17816 df-top 18506 df-bases 18508 df-topon 18509 df-cld 18626 df-ntr 18627 df-cls 18628

This theorem is referenced by: metnrmlem1a 20437 lebnumlem1 20536

W3C validator