# 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 ) =/= (/) )`