This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsndisj

Description: Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion clsndisj 
|- ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 simp1 
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> J e. Top )
3 simp2 
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> S C_ X )
4 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
5 4 sseld 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> P e. X ) )
6 5 3impia 
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> P e. X )
7 simp3 
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> P e. ( ( cls ` J ) ` S ) )
8 1 elcls 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
9 8 biimpa 
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ P e. ( ( cls ` J ) ` S ) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) )
10 2 3 6 7 9 syl31anc 
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) )
11 eleq2 
 |-  ( x = U -> ( P e. x <-> P e. U ) )
12 ineq1 
 |-  ( x = U -> ( x i^i S ) = ( U i^i S ) )
13 12 neeq1d 
 |-  ( x = U -> ( ( x i^i S ) =/= (/) <-> ( U i^i S ) =/= (/) ) )
14 11 13 imbi12d 
 |-  ( x = U -> ( ( P e. x -> ( x i^i S ) =/= (/) ) <-> ( P e. U -> ( U i^i S ) =/= (/) ) ) )
15 14 rspccv 
 |-  ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( U e. J -> ( P e. U -> ( U i^i S ) =/= (/) ) ) )
16 15 imp32 
 |-  ( ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )
17 10 16 sylan 
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )