neindisj2 - Metamath Proof Explorer

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

Theorem neindisj2 20216

Description: A point

belongs to the closure of a set

iff every neighborhood of

meets

. (Contributed by FL, 15-Sep-2013.)

**Hypothesis**
Ref	Expression
tpnei.1

**Assertion**
Ref	Expression
neindisj2	$/\$ $/\$

Distinct variable groups:

Proof of Theorem neindisj2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tpnei.1	. . 3
2	1	elcls 20166	. 2 $/\$ $/\$
3	1	isneip 20198	. . . . . . . 8 $/\$ $/\$ $/\$
4		r19.29r 2913	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5		pm3.35 597	. . . . . . . . . . . . . . . 16 $/\$
6		ssrin 3648	. . . . . . . . . . . . . . . . . 18
7		sseq2 3440	. . . . . . . . . . . . . . . . . . 19
8		ss0 3768	. . . . . . . . . . . . . . . . . . 19
9	7, 8	syl6bi 236	. . . . . . . . . . . . . . . . . 18
10	6, 9	syl5com 30	. . . . . . . . . . . . . . . . 17
11	10	necon3d 2664	. . . . . . . . . . . . . . . 16
12	5, 11	syl5com 30	. . . . . . . . . . . . . . 15 $/\$
13	12	ex 441	. . . . . . . . . . . . . 14
14	13	com23 80	. . . . . . . . . . . . 13
15	14	imp31 439	. . . . . . . . . . . 12 $/\$ $/\$
16	15	rexlimivw 2869	. . . . . . . . . . 11 $/\$ $/\$
17	4, 16	syl 17	. . . . . . . . . 10 $/\$ $/\$
18	17	ex 441	. . . . . . . . 9 $/\$
19	18	adantl 473	. . . . . . . 8 $/\$ $/\$
20	3, 19	syl6bi 236	. . . . . . 7 $/\$
21	20	3adant2 1049	. . . . . 6 $/\$ $/\$
22	21	com23 80	. . . . 5 $/\$ $/\$
23	22	imp 436	. . . 4 $/\$ $/\$ $/\$
24	23	ralrimiv 2808	. . 3 $/\$ $/\$ $/\$
25		opnneip 20212	. . . . . . . . . 10 $/\$ $/\$
26		ineq1 3618	. . . . . . . . . . . . . . 15
27	26	neeq1d 2702	. . . . . . . . . . . . . 14
28	27	rspccva 3135	. . . . . . . . . . . . 13 $/\$
29		idd 24	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
30	29	3exp 1230	. . . . . . . . . . . . . 14 $/\$ $/\$
31	30	com14 90	. . . . . . . . . . . . 13 $/\$ $/\$
32	28, 31	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33	32	ex 441	. . . . . . . . . . 11 $/\$ $/\$
34	33	com3l 83	. . . . . . . . . 10 $/\$ $/\$
35	25, 34	mpcom 36	. . . . . . . . 9 $/\$ $/\$
36	35	3expia 1233	. . . . . . . 8 $/\$
37	36	com25 93	. . . . . . 7 $/\$
38	37	ex 441	. . . . . 6
39	38	com25 93	. . . . 5
40	39	3imp1 1246	. . . 4 $/\$ $/\$ $/\$
41	40	ralrimiv 2808	. . 3 $/\$ $/\$ $/\$
42	24, 41	impbida 850	. 2 $/\$ $/\$
43	2, 42	bitrd 261	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cin 3389

wss 3390

c0 3722

csn 3959

cuni 4190

cfv 5589

ctop 19994

ccl 20110

cnei 20190

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

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 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-ral 2761 df-rex 2762 df-reu 2763 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-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 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-id 4754 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-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-top 19998 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191

This theorem is referenced by: islp2 20238 trnei 20985 flimclsi 21071

W3C validator