Metamath Proof Explorer

Theorem fsubbas

Description: A condition for a set to generate a filter base. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fsubbas ( 𝑋 ∈ 𝑉 → ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 fbasne0 ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐴 ) ≠ ∅ )
2 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( fi ‘ 𝐴 ) = ∅ )
3 2 necon1ai ⊢ ( ( fi ‘ 𝐴 ) ≠ ∅ → 𝐴 ∈ V )
4 1 3 syl ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → 𝐴 ∈ V )
5 ssfii ⊢ ( 𝐴 ∈ V → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
6 4 5 syl ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
7 fbsspw ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
8 6 7 sstrd ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → 𝐴 ⊆ 𝒫 𝑋 )
9 fieq0 ⊢ ( 𝐴 ∈ V → ( 𝐴 = ∅ ↔ ( fi ‘ 𝐴 ) = ∅ ) )
10 9 necon3bid ⊢ ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ ↔ ( fi ‘ 𝐴 ) ≠ ∅ ) )
11 10 biimpar ⊢ ( ( 𝐴 ∈ V ∧ ( fi ‘ 𝐴 ) ≠ ∅ ) → 𝐴 ≠ ∅ )
12 4 1 11 syl2anc ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → 𝐴 ≠ ∅ )
13 0nelfb ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ ( fi ‘ 𝐴 ) )
14 8 12 13 3jca ⊢ ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) )
15 simpr1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝒫 𝑋 )
16 fipwss ⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
17 15 16 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
18 pwexg ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V )
19 18 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → 𝒫 𝑋 ∈ V )
20 19 15 ssexd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → 𝐴 ∈ V )
21 simpr2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → 𝐴 ≠ ∅ )
22 10 biimpa ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) → ( fi ‘ 𝐴 ) ≠ ∅ )
23 20 21 22 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ( fi ‘ 𝐴 ) ≠ ∅ )
24 simpr3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ¬ ∅ ∈ ( fi ‘ 𝐴 ) )
25 df-nel ⊢ ( ∅ ∉ ( fi ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( fi ‘ 𝐴 ) )
26 24 25 sylibr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ∅ ∉ ( fi ‘ 𝐴 ) )
27 fiin ⊢ ( ( 𝑥 ∈ ( fi ‘ 𝐴 ) ∧ 𝑦 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) )
28 ssid ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
29 sseq1 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
30 29 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
31 27 28 30 sylancl ⊢ ( ( 𝑥 ∈ ( fi ‘ 𝐴 ) ∧ 𝑦 ∈ ( fi ‘ 𝐴 ) ) → ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
32 31 rgen2 ⊢ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 )
33 32 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
34 23 26 33 3jca ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ( ( fi ‘ 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( fi ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
35 isfbas2 ⊢ ( 𝑋 ∈ 𝑉 → ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 ∧ ( ( fi ‘ 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( fi ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
36 35 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 ∧ ( ( fi ‘ 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( fi ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ∃ 𝑧 ∈ ( fi ‘ 𝐴 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
37 17 34 36 mpbir2and ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) → ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) )
38 37 ex ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) → ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ) )
39 14 38 impbid2 ⊢ ( 𝑋 ∈ 𝑉 → ( ( fi ‘ 𝐴 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ 𝐴 ) ) ) )