# 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}=\bigcup {J}$
Assertion clsndisj ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({U}\in {J}\wedge {P}\in {U}\right)\right)\to {U}\cap {S}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 simp1 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {J}\in \mathrm{Top}$
3 simp2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {S}\subseteq {X}$
4 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
5 4 sseld ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to {P}\in {X}\right)$
6 5 3impia ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {P}\in {X}$
7 simp3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)$
8 1 elcls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)$
9 8 biimpa ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)$
10 2 3 6 7 9 syl31anc ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)$
11 eleq2 ${⊢}{x}={U}\to \left({P}\in {x}↔{P}\in {U}\right)$
12 ineq1 ${⊢}{x}={U}\to {x}\cap {S}={U}\cap {S}$
13 12 neeq1d ${⊢}{x}={U}\to \left({x}\cap {S}\ne \varnothing ↔{U}\cap {S}\ne \varnothing \right)$
14 11 13 imbi12d ${⊢}{x}={U}\to \left(\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)↔\left({P}\in {U}\to {U}\cap {S}\ne \varnothing \right)\right)$
15 14 rspccv ${⊢}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to \left({U}\in {J}\to \left({P}\in {U}\to {U}\cap {S}\ne \varnothing \right)\right)$
16 15 imp32 ${⊢}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\wedge \left({U}\in {J}\wedge {P}\in {U}\right)\right)\to {U}\cap {S}\ne \varnothing$
17 10 16 sylan ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({U}\in {J}\wedge {P}\in {U}\right)\right)\to {U}\cap {S}\ne \varnothing$