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 21864

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 1046	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2		simprl 763	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
3		simprr 765	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
4		metdscn.j	. . . . . . . 8
5	4	mopni2 21501	. . . . . . 7 $/\$ $/\$
6	1, 2, 3, 5	syl3anc 1267	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
7		simprr 765	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		ssrin 3656	. . . . . . . 8
9	7, 8	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		rpgt0 11310	. . . . . . . . . 10
11		0re 9640	. . . . . . . . . . 11
12		rpre 11305	. . . . . . . . . . 11
13		ltnle 9710	. . . . . . . . . . 11 $/\$
14	11, 12, 13	sylancr 668	. . . . . . . . . 10
15	10, 14	mpbid 214	. . . . . . . . 9
16	15	ad2antrl 733	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simpllr 768	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	breq2d 4413	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	1	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simpl2 1011	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simpl3 1012	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
23	22	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		rpxr 11306	. . . . . . . . . . . . 13
25	24	ad2antrl 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		metdscn.f	. . . . . . . . . . . . 13 inf
27	26	metdsge 21859	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28	19, 21, 23, 25, 27	syl31anc 1270	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	18, 28	bitr3d 259	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		incom 3624	. . . . . . . . . . 11
31	30	eqeq1i 2455	. . . . . . . . . 10
32	29, 31	syl6bb 265	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	necon3bbid 2660	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	16, 33	mpbid 214	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		ssn0 3766	. . . . . . 7 $/\$
36	9, 34, 35	syl2anc 666	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 36	rexlimddv 2882	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	expr 619	. . . 4 $/\$ $/\$ $/\$ $/\$
39	38	ralrimiva 2801	. . 3 $/\$ $/\$ $/\$
40	4	mopntopon 21447	. . . . . . 7 TopOn
41	40	3ad2ant1 1028	. . . . . 6 $/\$ $/\$ TopOn
42	41	adantr 467	. . . . 5 $/\$ $/\$ $/\$ TopOn
43		topontop 19934	. . . . 5 TopOn
44	42, 43	syl 17	. . . 4 $/\$ $/\$ $/\$
45		toponuni 19935	. . . . . 6 TopOn
46	42, 45	syl 17	. . . . 5 $/\$ $/\$ $/\$
47	20, 46	sseqtrd 3467	. . . 4 $/\$ $/\$ $/\$
48	22, 46	eleqtrd 2530	. . . 4 $/\$ $/\$ $/\$
49		eqid 2450	. . . . 5
50	49	elcls 20082	. . . 4 $/\$ $/\$
51	44, 47, 48, 50	syl3anc 1267	. . 3 $/\$ $/\$ $/\$
52	39, 51	mpbird 236	. 2 $/\$ $/\$ $/\$
53		incom 3624	. . . . . . 7
54	26	metdsf 21858	. . . . . . . . . . . 12 $/\$
55	54	ffvelrnda 6020	. . . . . . . . . . 11 $/\$ $/\$
56	55	3impa 1202	. . . . . . . . . 10 $/\$ $/\$
57		elxrge0 11738	. . . . . . . . . . 11 $/\$
58	57	simplbi 462	. . . . . . . . . 10
59	56, 58	syl 17	. . . . . . . . 9 $/\$ $/\$
60		xrleid 11446	. . . . . . . . 9
61	59, 60	syl 17	. . . . . . . 8 $/\$ $/\$
62	26	metdsge 21859	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 62	mpdan 673	. . . . . . . 8 $/\$ $/\$
64	61, 63	mpbid 214	. . . . . . 7 $/\$ $/\$
65	53, 64	syl5eq 2496	. . . . . 6 $/\$ $/\$
66	65	adantr 467	. . . . 5 $/\$ $/\$ $/\$
67	41	ad2antrr 731	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ TopOn
68	67, 43	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpll2 1047	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
70	67, 45	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71	69, 70	sseqtrd 3467	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
72		simplr 761	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73		simpll1 1046	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74		simpll3 1048	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75	59	ad2antrr 731	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	4	blopn 21508	. . . . . . . . 9 $/\$ $/\$
77	73, 74, 75, 76	syl3anc 1267	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
78		simpr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79		xblcntr 21419	. . . . . . . . 9 $/\$ $/\$ $/\$
80	73, 74, 75, 78, 79	syl112anc 1271	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	49	clsndisj 20084	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	68, 71, 72, 77, 80, 81	syl32anc 1275	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	82	ex 436	. . . . . 6 $/\$ $/\$ $/\$
84	83	necon2bd 2639	. . . . 5 $/\$ $/\$ $/\$
85	66, 84	mpd 15	. . . 4 $/\$ $/\$ $/\$
86	57	simprbi 466	. . . . . . . 8
87	56, 86	syl 17	. . . . . . 7 $/\$ $/\$
88		0xr 9684	. . . . . . . 8
89		xrleloe 11440	. . . . . . . 8 $/\$ $\/$
90	88, 59, 89	sylancr 668	. . . . . . 7 $/\$ $/\$ $\/$
91	87, 90	mpbid 214	. . . . . 6 $/\$ $/\$ $\/$
92	91	adantr 467	. . . . 5 $/\$ $/\$ $/\$ $\/$
93	92	ord 379	. . . 4 $/\$ $/\$ $/\$
94	85, 93	mpd 15	. . 3 $/\$ $/\$ $/\$
95	94	eqcomd 2456	. 2 $/\$ $/\$ $/\$
96	52, 95	impbida 842	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621

wral 2736

wrex 2737

cin 3402

wss 3403

c0 3730

cuni 4197 class class class wbr 4401

cmpt 4460

crn 4834

cfv 5581 (class class class)co 6288 infcinf 7952

cr 9535

cc0 9536

cpnf 9669

cxr 9671

clt 9672

cle 9673

crp 11299

cicc 11635

cxmt 18948

cbl 18950

cmopn 18953

ctop 19910 TopOnctopon 19911

ccl 20026

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-iin 4280 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-map 7471 df-en 7567 df-dom 7568 df-sdom 7569 df-sup 7953 df-inf 7954 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-n0 10867 df-z 10935 df-uz 11157 df-q 11262 df-rp 11300 df-xneg 11406 df-xadd 11407 df-xmul 11408 df-icc 11639 df-topgen 15335 df-psmet 18955 df-xmet 18956 df-bl 18958 df-mopn 18959 df-top 19914 df-bases 19915 df-topon 19916 df-cld 20027 df-ntr 20028 df-cls 20029

This theorem is referenced by: metnrmlem1a 21868 lebnumlem1 21982

W3C validator