Metamath Proof Explorer


Theorem opnnei

Description: A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009)

Ref Expression
Assertion opnnei ( 𝐽 ∈ Top → ( 𝑆𝐽 ↔ ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 0opn ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
2 1 adantr ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ∅ ∈ 𝐽 )
3 eleq1 ( 𝑆 = ∅ → ( 𝑆𝐽 ↔ ∅ ∈ 𝐽 ) )
4 3 adantl ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ( 𝑆𝐽 ↔ ∅ ∈ 𝐽 ) )
5 2 4 mpbird ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → 𝑆𝐽 )
6 rzal ( 𝑆 = ∅ → ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
7 6 adantl ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
8 5 7 2thd ( ( 𝐽 ∈ Top ∧ 𝑆 = ∅ ) → ( 𝑆𝐽 ↔ ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
9 opnneip ( ( 𝐽 ∈ Top ∧ 𝑆𝐽𝑥𝑆 ) → 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
10 9 3expia ( ( 𝐽 ∈ Top ∧ 𝑆𝐽 ) → ( 𝑥𝑆𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
11 10 ralrimiv ( ( 𝐽 ∈ Top ∧ 𝑆𝐽 ) → ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
12 11 ex ( 𝐽 ∈ Top → ( 𝑆𝐽 → ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
13 12 adantr ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( 𝑆𝐽 → ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
14 df-ne ( 𝑆 ≠ ∅ ↔ ¬ 𝑆 = ∅ )
15 r19.2z ( ( 𝑆 ≠ ∅ ∧ ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
16 15 ex ( 𝑆 ≠ ∅ → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
17 14 16 sylbir ( ¬ 𝑆 = ∅ → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
18 eqid 𝐽 = 𝐽
19 18 neii1 ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑆 𝐽 )
20 19 ex ( 𝐽 ∈ Top → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 𝐽 ) )
21 20 rexlimdvw ( 𝐽 ∈ Top → ( ∃ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 𝐽 ) )
22 17 21 sylan9r ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆 𝐽 ) )
23 18 ntrss2 ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )
24 23 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )
25 vex 𝑥 ∈ V
26 25 snss ( 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
27 26 ralbii ( ∀ 𝑥𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
28 dfss3 ( 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
29 28 biimpri ( ∀ 𝑥𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
30 29 adantl ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ ∀ 𝑥𝑆 𝑥 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
31 27 30 sylan2br ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
32 24 31 eqssd ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
33 32 ex ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
34 25 snss ( 𝑥𝑆 ↔ { 𝑥 } ⊆ 𝑆 )
35 sstr2 ( { 𝑥 } ⊆ 𝑆 → ( 𝑆 𝐽 → { 𝑥 } ⊆ 𝐽 ) )
36 35 com12 ( 𝑆 𝐽 → ( { 𝑥 } ⊆ 𝑆 → { 𝑥 } ⊆ 𝐽 ) )
37 36 adantl ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( { 𝑥 } ⊆ 𝑆 → { 𝑥 } ⊆ 𝐽 ) )
38 34 37 syl5bi ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( 𝑥𝑆 → { 𝑥 } ⊆ 𝐽 ) )
39 38 imp ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ 𝑥𝑆 ) → { 𝑥 } ⊆ 𝐽 )
40 18 neiint ( ( 𝐽 ∈ Top ∧ { 𝑥 } ⊆ 𝐽𝑆 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
41 40 3com23 ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ∧ { 𝑥 } ⊆ 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
42 41 3expa ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ { 𝑥 } ⊆ 𝐽 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
43 39 42 syldan ( ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) ∧ 𝑥𝑆 ) → ( 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
44 43 ralbidva ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↔ ∀ 𝑥𝑆 { 𝑥 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
45 18 isopn3 ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( 𝑆𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
46 33 44 45 3imtr4d ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆𝐽 ) )
47 46 ex ( 𝐽 ∈ Top → ( 𝑆 𝐽 → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆𝐽 ) ) )
48 47 com23 ( 𝐽 ∈ Top → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑆 𝐽𝑆𝐽 ) ) )
49 48 adantr ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ( 𝑆 𝐽𝑆𝐽 ) ) )
50 22 49 mpdd ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → 𝑆𝐽 ) )
51 13 50 impbid ( ( 𝐽 ∈ Top ∧ ¬ 𝑆 = ∅ ) → ( 𝑆𝐽 ↔ ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )
52 8 51 pm2.61dan ( 𝐽 ∈ Top → ( 𝑆𝐽 ↔ ∀ 𝑥𝑆 𝑆 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) )