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 e. V -> ( ( fi ` A ) e. ( fBas ` X ) <-> ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 fbasne0 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> ( fi ` A ) =/= (/) )
2 fvprc 
 |-  ( -. A e. _V -> ( fi ` A ) = (/) )
3 2 necon1ai 
 |-  ( ( fi ` A ) =/= (/) -> A e. _V )
4 1 3 syl 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> A e. _V )
5 ssfii 
 |-  ( A e. _V -> A C_ ( fi ` A ) )
6 4 5 syl 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> A C_ ( fi ` A ) )
7 fbsspw 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> ( fi ` A ) C_ ~P X )
8 6 7 sstrd 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> A C_ ~P X )
9 fieq0 
 |-  ( A e. _V -> ( A = (/) <-> ( fi ` A ) = (/) ) )
10 9 necon3bid 
 |-  ( A e. _V -> ( A =/= (/) <-> ( fi ` A ) =/= (/) ) )
11 10 biimpar 
 |-  ( ( A e. _V /\ ( fi ` A ) =/= (/) ) -> A =/= (/) )
12 4 1 11 syl2anc 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> A =/= (/) )
13 0nelfb 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> -. (/) e. ( fi ` A ) )
14 8 12 13 3jca 
 |-  ( ( fi ` A ) e. ( fBas ` X ) -> ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) )
15 simpr1 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> A C_ ~P X )
16 fipwss 
 |-  ( A C_ ~P X -> ( fi ` A ) C_ ~P X )
17 15 16 syl 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ( fi ` A ) C_ ~P X )
18 pwexg 
 |-  ( X e. V -> ~P X e. _V )
19 18 adantr 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ~P X e. _V )
20 19 15 ssexd 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> A e. _V )
21 simpr2 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> A =/= (/) )
22 10 biimpa 
 |-  ( ( A e. _V /\ A =/= (/) ) -> ( fi ` A ) =/= (/) )
23 20 21 22 syl2anc 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ( fi ` A ) =/= (/) )
24 simpr3 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> -. (/) e. ( fi ` A ) )
25 df-nel 
 |-  ( (/) e/ ( fi ` A ) <-> -. (/) e. ( fi ` A ) )
26 24 25 sylibr 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> (/) e/ ( fi ` A ) )
27 fiin 
 |-  ( ( x e. ( fi ` A ) /\ y e. ( fi ` A ) ) -> ( x i^i y ) e. ( fi ` A ) )
28 ssid 
 |-  ( x i^i y ) C_ ( x i^i y )
29 sseq1 
 |-  ( z = ( x i^i y ) -> ( z C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
30 29 rspcev 
 |-  ( ( ( x i^i y ) e. ( fi ` A ) /\ ( x i^i y ) C_ ( x i^i y ) ) -> E. z e. ( fi ` A ) z C_ ( x i^i y ) )
31 27 28 30 sylancl 
 |-  ( ( x e. ( fi ` A ) /\ y e. ( fi ` A ) ) -> E. z e. ( fi ` A ) z C_ ( x i^i y ) )
32 31 rgen2 
 |-  A. x e. ( fi ` A ) A. y e. ( fi ` A ) E. z e. ( fi ` A ) z C_ ( x i^i y )
33 32 a1i 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> A. x e. ( fi ` A ) A. y e. ( fi ` A ) E. z e. ( fi ` A ) z C_ ( x i^i y ) )
34 23 26 33 3jca 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ( ( fi ` A ) =/= (/) /\ (/) e/ ( fi ` A ) /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) E. z e. ( fi ` A ) z C_ ( x i^i y ) ) )
35 isfbas2 
 |-  ( X e. V -> ( ( fi ` A ) e. ( fBas ` X ) <-> ( ( fi ` A ) C_ ~P X /\ ( ( fi ` A ) =/= (/) /\ (/) e/ ( fi ` A ) /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) E. z e. ( fi ` A ) z C_ ( x i^i y ) ) ) ) )
36 35 adantr 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ( ( fi ` A ) e. ( fBas ` X ) <-> ( ( fi ` A ) C_ ~P X /\ ( ( fi ` A ) =/= (/) /\ (/) e/ ( fi ` A ) /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) E. z e. ( fi ` A ) z C_ ( x i^i y ) ) ) ) )
37 17 34 36 mpbir2and 
 |-  ( ( X e. V /\ ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) -> ( fi ` A ) e. ( fBas ` X ) )
38 37 ex 
 |-  ( X e. V -> ( ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) -> ( fi ` A ) e. ( fBas ` X ) ) )
39 14 38 impbid2 
 |-  ( X e. V -> ( ( fi ` A ) e. ( fBas ` X ) <-> ( A C_ ~P X /\ A =/= (/) /\ -. (/) e. ( fi ` A ) ) ) )