# Metamath Proof Explorer

## Theorem elcls

Description: Membership in a closure. Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 22-Feb-2007)

Ref Expression
Hypothesis clscld.1 ${⊢}{X}=\bigcup {J}$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 1 cmclsopn ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\in {J}$
3 2 3adant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to {X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\in {J}$
4 3 adantr ${⊢}\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 {X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\in {J}$
5 eldif ${⊢}{P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)↔\left({P}\in {X}\wedge ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
6 5 biimpri ${⊢}\left({P}\in {X}\wedge ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
7 6 3ad2antl3 ${⊢}\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 {P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
8 simpr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq {X}$
9 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
10 8 9 ssind ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq {X}\cap \mathrm{cls}\left({J}\right)\left({S}\right)$
11 dfin4 ${⊢}{X}\cap \mathrm{cls}\left({J}\right)\left({S}\right)={X}\setminus \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
12 10 11 sseqtrdi ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq {X}\setminus \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
13 reldisj ${⊢}{S}\subseteq {X}\to \left({S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing ↔{S}\subseteq {X}\setminus \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
14 13 adantl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing ↔{S}\subseteq {X}\setminus \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
15 12 14 mpbird ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing$
16 nne ${⊢}¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing ↔\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}=\varnothing$
17 incom ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}={S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
18 17 eqeq1i ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}=\varnothing ↔{S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing$
19 16 18 bitri ${⊢}¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing ↔{S}\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)=\varnothing$
20 15 19 sylibr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to ¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing$
21 20 3adant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to ¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing$
22 21 adantr ${⊢}\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 ¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing$
23 eleq2 ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\to \left({P}\in {x}↔{P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
24 ineq1 ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\to {x}\cap {S}=\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}$
25 24 neeq1d ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\to \left({x}\cap {S}\ne \varnothing ↔\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing \right)$
26 25 notbid ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\to \left(¬{x}\cap {S}\ne \varnothing ↔¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing \right)$
27 23 26 anbi12d ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\to \left(\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)↔\left({P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge ¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing \right)\right)$
28 27 rspcev ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\in {J}\wedge \left({P}\in \left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge ¬\left({X}\setminus \mathrm{cls}\left({J}\right)\left({S}\right)\right)\cap {S}\ne \varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)$
29 4 7 22 28 syl12anc ${⊢}\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 \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)$
30 incom ${⊢}{S}\cap {x}={x}\cap {S}$
31 30 eqeq1i ${⊢}{S}\cap {x}=\varnothing ↔{x}\cap {S}=\varnothing$
32 df-ne ${⊢}{x}\cap {S}\ne \varnothing ↔¬{x}\cap {S}=\varnothing$
33 32 con2bii ${⊢}{x}\cap {S}=\varnothing ↔¬{x}\cap {S}\ne \varnothing$
34 31 33 bitri ${⊢}{S}\cap {x}=\varnothing ↔¬{x}\cap {S}\ne \varnothing$
35 1 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\to {X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)$
36 35 adantlr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\to {X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)$
37 reldisj ${⊢}{S}\subseteq {X}\to \left({S}\cap {x}=\varnothing ↔{S}\subseteq {X}\setminus {x}\right)$
38 37 biimpa ${⊢}\left({S}\subseteq {X}\wedge {S}\cap {x}=\varnothing \right)\to {S}\subseteq {X}\setminus {x}$
39 38 ad4ant24 ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge {S}\cap {x}=\varnothing \right)\to {S}\subseteq {X}\setminus {x}$
40 1 clsss2 ${⊢}\left({X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {X}\setminus {x}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}\setminus {x}$
41 36 39 40 syl2an2r ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge {S}\cap {x}=\varnothing \right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}\setminus {x}$
42 41 sseld ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge {S}\cap {x}=\varnothing \right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to {P}\in \left({X}\setminus {x}\right)\right)$
43 eldifn ${⊢}{P}\in \left({X}\setminus {x}\right)\to ¬{P}\in {x}$
44 42 43 syl6 ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge {S}\cap {x}=\varnothing \right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to ¬{P}\in {x}\right)$
45 44 con2d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge {S}\cap {x}=\varnothing \right)\to \left({P}\in {x}\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
46 34 45 sylan2br ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in {J}\right)\wedge ¬{x}\cap {S}\ne \varnothing \right)\to \left({P}\in {x}\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
47 46 exp31 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({x}\in {J}\to \left(¬{x}\cap {S}\ne \varnothing \to \left({P}\in {x}\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\right)$
48 47 com34 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({x}\in {J}\to \left({P}\in {x}\to \left(¬{x}\cap {S}\ne \varnothing \to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\right)$
49 48 imp4a ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({x}\in {J}\to \left(\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
50 49 rexlimdv ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)$
51 50 imp ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)\right)\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)$
52 51 3adantl3 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)\right)\to ¬{P}\in \mathrm{cls}\left({J}\right)\left({S}\right)$
53 29 52 impbida ${⊢}\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)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)\right)$
54 rexanali ${⊢}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge ¬{x}\cap {S}\ne \varnothing \right)↔¬\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)$
55 53 54 syl6bb ${⊢}\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)$
56 55 con4bid ${⊢}\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)$