This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snfbas

Description: Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion snfbas 
|- ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> { A } e. ( fBas ` B ) )

Proof

Step Hyp Ref Expression
1 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
2 1 3adant2 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> A e. _V )
3 simp2 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> A =/= (/) )
4 snfil 
 |-  ( ( A e. _V /\ A =/= (/) ) -> { A } e. ( Fil ` A ) )
5 2 3 4 syl2anc 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> { A } e. ( Fil ` A ) )
6 filfbas 
 |-  ( { A } e. ( Fil ` A ) -> { A } e. ( fBas ` A ) )
7 5 6 syl 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> { A } e. ( fBas ` A ) )
8 simp1 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> A C_ B )
9 elpw2g 
 |-  ( B e. V -> ( A e. ~P B <-> A C_ B ) )
10 9 3ad2ant3 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> ( A e. ~P B <-> A C_ B ) )
11 8 10 mpbird 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> A e. ~P B )
12 11 snssd 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> { A } C_ ~P B )
13 simp3 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> B e. V )
14 fbasweak 
 |-  ( ( { A } e. ( fBas ` A ) /\ { A } C_ ~P B /\ B e. V ) -> { A } e. ( fBas ` B ) )
15 7 12 13 14 syl3anc 
 |-  ( ( A C_ B /\ A =/= (/) /\ B e. V ) -> { A } e. ( fBas ` B ) )