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 ⊢ X ∈ V → fi ⁡ A ∈ fBas ⁡ X ↔ A ⊆ 𝒫 X ∧ A ≠ ∅ ∧ ¬ ∅ ∈ fi ⁡ A

Proof

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