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 ) )