Metamath Proof Explorer

Theorem neips

Description: A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 16-Nov-2006)

Ref Expression
Hypothesis neips.1 ⊢ 𝑋 = ∪ 𝐽
Assertion neips ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )

Proof

Step Hyp Ref Expression
1 neips.1 ⊢ 𝑋 = ∪ 𝐽
2 snssi ⊢ ( 𝑝 ∈ 𝑆 → { 𝑝 } ⊆ 𝑆 )
3 neiss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ { 𝑝 } ⊆ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) )
4 2 3 syl3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑝 ∈ 𝑆 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) )
5 4 3exp ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ( 𝑝 ∈ 𝑆 → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) ) )
6 5 ralrimdv ⊢ ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
7 6 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
8 r19.28zv ⊢ ( 𝑆 ≠ ∅ → ( ∀ 𝑝 ∈ 𝑆 ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ∀ 𝑝 ∈ 𝑆 ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
10 ssrab2 ⊢ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝐽
11 uniopn ⊢ ( ( 𝐽 ∈ Top ∧ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝐽 ) → ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∈ 𝐽 )
12 10 11 mpan2 ⊢ ( 𝐽 ∈ Top → ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∈ 𝐽 )
13 12 ad2antrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∈ 𝐽 )
14 sseq1 ⊢ ( 𝑣 = 𝑔 → ( 𝑣 ⊆ 𝑁 ↔ 𝑔 ⊆ 𝑁 ) )
15 14 elrab ⊢ ( 𝑔 ∈ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ↔ ( 𝑔 ∈ 𝐽 ∧ 𝑔 ⊆ 𝑁 ) )
16 elunii ⊢ ( ( 𝑝 ∈ 𝑔 ∧ 𝑔 ∈ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ) → 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
17 15 16 sylan2br ⊢ ( ( 𝑝 ∈ 𝑔 ∧ ( 𝑔 ∈ 𝐽 ∧ 𝑔 ⊆ 𝑁 ) ) → 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
18 17 an12s ⊢ ( ( 𝑔 ∈ 𝐽 ∧ ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
19 18 rexlimiva ⊢ ( ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
20 19 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∀ 𝑝 ∈ 𝑆 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
21 dfss3 ⊢ ( 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ↔ ∀ 𝑝 ∈ 𝑆 𝑝 ∈ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
22 20 21 sylibr ⊢ ( ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
23 22 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } )
24 unissb ⊢ ( ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁 ↔ ∀ ℎ ∈ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ℎ ⊆ 𝑁 )
25 sseq1 ⊢ ( 𝑣 = ℎ → ( 𝑣 ⊆ 𝑁 ↔ ℎ ⊆ 𝑁 ) )
26 25 elrab ⊢ ( ℎ ∈ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ↔ ( ℎ ∈ 𝐽 ∧ ℎ ⊆ 𝑁 ) )
27 26 simprbi ⊢ ( ℎ ∈ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } → ℎ ⊆ 𝑁 )
28 24 27 mprgbir ⊢ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁
29 23 28 jctir ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∧ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁 ) )
30 sseq2 ⊢ ( ℎ = ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } → ( 𝑆 ⊆ ℎ ↔ 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ) )
31 sseq1 ⊢ ( ℎ = ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } → ( ℎ ⊆ 𝑁 ↔ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁 ) )
32 30 31 anbi12d ⊢ ( ℎ = ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } → ( ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ↔ ( 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∧ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁 ) ) )
33 32 rspcev ⊢ ( ( ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∈ 𝐽 ∧ ( 𝑆 ⊆ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ∧ ∪ { 𝑣 ∈ 𝐽 ∣ 𝑣 ⊆ 𝑁 } ⊆ 𝑁 ) ) → ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) )
34 13 29 33 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) )
35 34 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) → ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) )
36 35 anim2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑁 ⊆ 𝑋 ∧ ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ) )
37 36 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑆 ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑁 ⊆ 𝑋 ∧ ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ) )
38 9 37 sylbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ∀ 𝑝 ∈ 𝑆 ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) → ( 𝑁 ⊆ 𝑋 ∧ ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ) )
39 ssel2 ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑆 ) → 𝑝 ∈ 𝑋 )
40 1 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
41 39 40 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ 𝑝 ∈ 𝑆 ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
42 41 anassrs ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑆 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
43 42 ralbidva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ∀ 𝑝 ∈ 𝑆 ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
44 43 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ∀ 𝑝 ∈ 𝑆 ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑝 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) )
45 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ) )
46 45 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ) )
47 38 44 46 3imtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
48 7 47 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑝 ∈ 𝑆 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )