Metamath Proof Explorer

Theorem fbdmn0

Description: The domain of a filter base is nonempty. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbdmn0 
|- ( F e. ( fBas ` B ) -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 0nelfb 
 |-  ( F e. ( fBas ` B ) -> -. (/) e. F )
2 fveq2 
 |-  ( B = (/) -> ( fBas ` B ) = ( fBas ` (/) ) )
3 2 eleq2d 
 |-  ( B = (/) -> ( F e. ( fBas ` B ) <-> F e. ( fBas ` (/) ) ) )
4 3 biimpd 
 |-  ( B = (/) -> ( F e. ( fBas ` B ) -> F e. ( fBas ` (/) ) ) )
5 fbasne0 
 |-  ( F e. ( fBas ` (/) ) -> F =/= (/) )
6 n0 
 |-  ( F =/= (/) <-> E. x x e. F )
7 5 6 sylib 
 |-  ( F e. ( fBas ` (/) ) -> E. x x e. F )
8 fbelss 
 |-  ( ( F e. ( fBas ` (/) ) /\ x e. F ) -> x C_ (/) )
9 ss0 
 |-  ( x C_ (/) -> x = (/) )
10 8 9 syl 
 |-  ( ( F e. ( fBas ` (/) ) /\ x e. F ) -> x = (/) )
11 simpr 
 |-  ( ( F e. ( fBas ` (/) ) /\ x e. F ) -> x e. F )
12 10 11 eqeltrrd 
 |-  ( ( F e. ( fBas ` (/) ) /\ x e. F ) -> (/) e. F )
13 7 12 exlimddv 
 |-  ( F e. ( fBas ` (/) ) -> (/) e. F )
14 4 13 syl6com 
 |-  ( F e. ( fBas ` B ) -> ( B = (/) -> (/) e. F ) )
15 14 necon3bd 
 |-  ( F e. ( fBas ` B ) -> ( -. (/) e. F -> B =/= (/) ) )
16 1 15 mpd 
 |-  ( F e. ( fBas ` B ) -> B =/= (/) )