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 syl5bi ( ( 𝐽 ∈ 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 ‘ 𝑋 ) )