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 ⊢ 𝑋 = ∪ 𝐽
Assertion elcls ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 cmclsopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )
3 2 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )
4 3 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )
5 eldif ⊢ ( 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( 𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
6 5 biimpri ⊢ ( ( 𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 6 3ad2antl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
8 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 )
9 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
10 8 9 ssind ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( 𝑋 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
11 dfin4 ⊢ ( 𝑋 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
12 10 11 sseqtrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
13 reldisj ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ ↔ 𝑆 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
14 13 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ ↔ 𝑆 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
15 12 14 mpbird ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ )
16 nne ⊢ ( ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ↔ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) = ∅ )
17 incom ⊢ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) = ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
18 17 eqeq1i ⊢ ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) = ∅ ↔ ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ )
19 16 18 bitri ⊢ ( ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ↔ ( 𝑆 ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ )
20 15 19 sylibr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ )
21 20 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ )
22 21 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ )
23 eleq2 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
24 ineq1 ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑆 ) = ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) )
25 24 neeq1d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ↔ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ) )
26 25 notbid ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ↔ ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ) )
27 23 26 anbi12d ⊢ ( 𝑥 = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ↔ ( 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ) ) )
28 27 rspcev ⊢ ( ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ¬ ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∩ 𝑆 ) ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
29 4 7 22 28 syl12anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
30 incom ⊢ ( 𝑆 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑆 )
31 30 eqeq1i ⊢ ( ( 𝑆 ∩ 𝑥 ) = ∅ ↔ ( 𝑥 ∩ 𝑆 ) = ∅ )
32 df-ne ⊢ ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ↔ ¬ ( 𝑥 ∩ 𝑆 ) = ∅ )
33 32 con2bii ⊢ ( ( 𝑥 ∩ 𝑆 ) = ∅ ↔ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
34 31 33 bitri ⊢ ( ( 𝑆 ∩ 𝑥 ) = ∅ ↔ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
35 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
36 35 adantlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
37 reldisj ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑆 ∩ 𝑥 ) = ∅ ↔ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
38 37 biimpa ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) )
39 38 ad4ant24 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) )
40 1 clsss2 ⊢ ( ( ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑥 ) )
41 36 39 40 syl2an2r ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( 𝑋 ∖ 𝑥 ) )
42 41 sseld ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑃 ∈ ( 𝑋 ∖ 𝑥 ) ) )
43 eldifn ⊢ ( 𝑃 ∈ ( 𝑋 ∖ 𝑥 ) → ¬ 𝑃 ∈ 𝑥 )
44 42 43 syl6 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ¬ 𝑃 ∈ 𝑥 ) )
45 44 con2d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑆 ∩ 𝑥 ) = ∅ ) → ( 𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
46 34 45 sylan2br ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
47 46 exp31 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 → ( ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ( 𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
48 47 com34 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 → ( 𝑃 ∈ 𝑥 → ( ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
49 48 imp4a ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 → ( ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
50 49 rexlimdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
51 50 imp ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
52 51 3adantl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
53 29 52 impbida ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
54 rexanali ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ¬ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ↔ ¬ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
55 53 54 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ¬ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
56 55 con4bid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )