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 ‘ 𝐽 ) ‘ { 𝑥 } ) ) )