Metamath Proof Explorer

Theorem opnfbas

Description: The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 7-Aug-2015)

Ref Expression
Hypothesis opnfbas.1 ⊢ 𝑋 = ∪ 𝐽
Assertion opnfbas ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 opnfbas.1 ⊢ 𝑋 = ∪ 𝐽
2 ssrab2 ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝐽
3 1 eqimss2i ⊢ ∪ 𝐽 ⊆ 𝑋
4 sspwuni ⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 )
5 3 4 mpbir ⊢ 𝐽 ⊆ 𝒫 𝑋
6 2 5 sstri ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋
7 6 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 )
8 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
9 8 anim1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) )
10 9 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) )
11 sseq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋 ) )
12 11 elrab ⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) )
13 10 12 sylibr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝑋 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } )
14 13 ne0d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ )
15 ss0 ⊢ ( 𝑆 ⊆ ∅ → 𝑆 = ∅ )
16 15 necon3ai ⊢ ( 𝑆 ≠ ∅ → ¬ 𝑆 ⊆ ∅ )
17 16 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ¬ 𝑆 ⊆ ∅ )
18 17 intnand ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) )
19 df-nel ⊢ ( ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ¬ ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } )
20 sseq2 ⊢ ( 𝑥 = ∅ → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ ∅ ) )
21 20 elrab ⊢ ( ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) )
22 21 notbii ⊢ ( ¬ ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) )
23 19 22 bitr2i ⊢ ( ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) ↔ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } )
24 18 23 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } )
25 sseq2 ⊢ ( 𝑥 = 𝑟 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑟 ) )
26 25 elrab ⊢ ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) )
27 sseq2 ⊢ ( 𝑥 = 𝑠 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑠 ) )
28 27 elrab ⊢ ( 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) )
29 26 28 anbi12i ⊢ ( ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) ↔ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) )
30 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝐽 ∈ Top )
31 simprll ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑟 ∈ 𝐽 )
32 simprrl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑠 ∈ 𝐽 )
33 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
34 30 31 32 33 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
35 ssin ⊢ ( ( 𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠 ) ↔ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) )
36 35 biimpi ⊢ ( ( 𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠 ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) )
37 36 ad2ant2l ⊢ ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) )
38 37 adantl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) )
39 34 38 jca ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
40 39 3ad2antl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
41 sseq2 ⊢ ( 𝑥 = ( 𝑟 ∩ 𝑠 ) → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
42 41 elrab ⊢ ( ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
43 40 42 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } )
44 ssid ⊢ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 )
45 sseq1 ⊢ ( 𝑡 = ( 𝑟 ∩ 𝑠 ) → ( 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ↔ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) )
46 45 rspcev ⊢ ( ( ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
47 43 44 46 sylancl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
48 47 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
49 29 48 biimtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
50 49 ralrimivv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) )
51 14 24 50 3jca ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
52 isfbas2 ⊢ ( 𝑋 ∈ 𝐽 → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
53 8 52 syl ⊢ ( 𝐽 ∈ Top → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
54 53 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
55 7 51 54 mpbir2and ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) )