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⁡Az⊆x∩y
31 27 28 30 sylancl ⊢x∈fi⁡A∧y∈fi⁡A→∃z∈fi⁡Az⊆x∩y
32 31 rgen2 ⊢∀x∈fi⁡A∀y∈fi⁡A∃z∈fi⁡Az⊆x∩y
33 32 a1i ⊢X∈V∧A⊆𝒫X∧A≠∅∧¬∅∈fi⁡A→∀x∈fi⁡A∀y∈fi⁡A∃z∈fi⁡Az⊆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⁡Az⊆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⁡Az⊆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⁡Az⊆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