Metamath Proof Explorer

Theorem neindisj2

Description: A point P belongs to the closure of a set S iff every neighborhood of P meets S . (Contributed by FL, 15-Sep-2013)

Ref Expression
Hypothesis tpnei.1 ⊢ 𝑋 = ∪ 𝐽
Assertion neindisj2 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 ⊢ 𝑋 = ∪ 𝐽
2 1 elcls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
3 1 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑛 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ) ) )
4 r19.29r ⊢ ( ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ∧ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
5 pm3.35 ⊢ ( ( 𝑃 ∈ 𝑥 ∧ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
6 ssrin ⊢ ( 𝑥 ⊆ 𝑛 → ( 𝑥 ∩ 𝑆 ) ⊆ ( 𝑛 ∩ 𝑆 ) )
7 sseq2 ⊢ ( ( 𝑛 ∩ 𝑆 ) = ∅ → ( ( 𝑥 ∩ 𝑆 ) ⊆ ( 𝑛 ∩ 𝑆 ) ↔ ( 𝑥 ∩ 𝑆 ) ⊆ ∅ ) )
8 ss0 ⊢ ( ( 𝑥 ∩ 𝑆 ) ⊆ ∅ → ( 𝑥 ∩ 𝑆 ) = ∅ )
9 7 8 biimtrdi ⊢ ( ( 𝑛 ∩ 𝑆 ) = ∅ → ( ( 𝑥 ∩ 𝑆 ) ⊆ ( 𝑛 ∩ 𝑆 ) → ( 𝑥 ∩ 𝑆 ) = ∅ ) )
10 6 9 syl5com ⊢ ( 𝑥 ⊆ 𝑛 → ( ( 𝑛 ∩ 𝑆 ) = ∅ → ( 𝑥 ∩ 𝑆 ) = ∅ ) )
11 10 necon3d ⊢ ( 𝑥 ⊆ 𝑛 → ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
12 5 11 syl5com ⊢ ( ( 𝑃 ∈ 𝑥 ∧ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑥 ⊆ 𝑛 → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
13 12 ex ⊢ ( 𝑃 ∈ 𝑥 → ( ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑥 ⊆ 𝑛 → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) ) )
14 13 com23 ⊢ ( 𝑃 ∈ 𝑥 → ( 𝑥 ⊆ 𝑛 → ( ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) ) )
15 14 imp31 ⊢ ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ∧ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ )
16 15 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐽 ( ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ∧ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ )
17 4 16 syl ⊢ ( ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ )
18 17 ex ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
19 18 adantl ⊢ ( ( 𝑛 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑛 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
20 3 19 biimtrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) ) )
21 20 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) ) )
22 21 com23 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) ) )
23 22 imp ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
24 23 ralrimiv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ )
25 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
26 ineq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 ∩ 𝑆 ) = ( 𝑥 ∩ 𝑆 ) )
27 26 neeq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑛 ∩ 𝑆 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
28 27 rspccva ⊢ ( ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
29 idd ⊢ ( ( 𝑃 ∈ 𝑋 ∧ ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
30 29 3exp ⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( 𝑆 ⊆ 𝑋 → ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )
31 30 com14 ⊢ ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ → ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )
32 28 31 syl ⊢ ( ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )
33 32 ex ⊢ ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) )
34 33 com3l ⊢ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) )
35 25 34 mpcom ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )
36 35 3expia ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑥 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) )
37 36 com25 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑋 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) )
38 37 ex ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 → ( 𝑃 ∈ 𝑋 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) ) )
39 38 com25 ⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 → ( 𝑃 ∈ 𝑋 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ → ( 𝑥 ∈ 𝐽 → ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) ) ) )
40 39 3imp1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑥 ∈ 𝐽 → ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
41 40 ralrimiv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) → ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
42 24 41 impbida ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )
43 2 42 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛 ∩ 𝑆 ) ≠ ∅ ) )