Metamath Proof Explorer

Theorem neifil

Description: The neighborhoods of a nonempty set is a filter. Example 2 of BourbakiTop1 p. I.36. (Contributed by FL, 18-Sep-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion neifil ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
2 1 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 = ∪ 𝐽 )
3 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
4 3 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐽 ∈ Top )
5 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 )
6 5 2 sseqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ∪ 𝐽 )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 7 neiuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ∪ 𝐽 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
9 4 6 8 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∪ 𝐽 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
10 2 9 eqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
11 eqimss2 ⊢ ( 𝑋 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
12 10 11 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
13 sspwuni ⊢ ( ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 ↔ ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
14 12 13 sylibr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 )
15 14 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 )
16 0nnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ≠ ∅ ) → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
17 3 16 sylan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ≠ ∅ ) → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
18 17 3adant2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
19 7 tpnei ⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ ∪ 𝐽 ↔ ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
20 19 biimpa ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
21 4 6 20 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
22 2 21 eqeltrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
23 22 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
24 15 18 23 3jca ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
25 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
26 4 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝐽 ∈ Top )
27 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
28 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ⊆ 𝑥 )
29 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ⊆ 𝑋 )
30 2 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑋 = ∪ 𝐽 )
31 29 30 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ⊆ ∪ 𝐽 )
32 7 ssnei2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ ∪ 𝐽 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
33 26 27 28 31 32 syl22anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
34 33 rexlimdvaa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
35 25 34 sylan2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
36 35 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
37 36 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
38 innei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
39 38 3expib ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
40 3 39 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
41 40 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
42 41 ralrimivv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
43 isfil2 ⊢ ( ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Fil ‘ 𝑋 ) ↔ ( ( ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
44 24 37 42 43 syl3anbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Fil ‘ 𝑋 ) )