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 syl6bi ( ( 𝑛𝑆 ) = ∅ → ( ( 𝑥𝑆 ) ⊆ ( 𝑛𝑆 ) → ( 𝑥𝑆 ) = ∅ ) )
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 syl6bi ( ( 𝐽 ∈ 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 ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑛𝑆 ) ≠ ∅ ) )