Metamath Proof Explorer


Theorem neindisj

Description: Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis neips.1 X = J
Assertion neindisj J Top S X P cls J S N nei J P N S

Proof

Step Hyp Ref Expression
1 neips.1 X = J
2 1 clsss3 J Top S X cls J S X
3 2 sseld J Top S X P cls J S P X
4 3 impr J Top S X P cls J S P X
5 1 isneip J Top P X N nei J P N X g J P g g N
6 4 5 syldan J Top S X P cls J S N nei J P N X g J P g g N
7 3anass J Top S X P cls J S J Top S X P cls J S
8 1 clsndisj J Top S X P cls J S g J P g g S
9 7 8 sylanbr J Top S X P cls J S g J P g g S
10 9 anassrs J Top S X P cls J S g J P g g S
11 10 adantllr J Top S X P cls J S N X g J P g g S
12 11 adantrr J Top S X P cls J S N X g J P g g N g S
13 ssdisj g N N S = g S =
14 13 ex g N N S = g S =
15 14 necon3d g N g S N S
16 15 ad2antll J Top S X P cls J S N X g J P g g N g S N S
17 12 16 mpd J Top S X P cls J S N X g J P g g N N S
18 17 rexlimdva2 J Top S X P cls J S N X g J P g g N N S
19 18 expimpd J Top S X P cls J S N X g J P g g N N S
20 6 19 sylbid J Top S X P cls J S N nei J P N S
21 20 exp32 J Top S X P cls J S N nei J P N S
22 21 imp43 J Top S X P cls J S N nei J P N S