Metamath Proof Explorer

Theorem fbasweak

Description: A filter base on any set is also a filter base on any larger set. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbasweak 
|- ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> F e. ( fBas ` Y ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> F C_ ~P Y )
2 simp1 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> F e. ( fBas ` X ) )
3 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
4 3 3ad2ant1 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> X e. dom fBas )
5 isfbas 
 |-  ( X e. dom fBas -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
6 4 5 syl 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
7 2 6 mpbid 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) )
8 7 simprd 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) )
9 isfbas 
 |-  ( Y e. V -> ( F e. ( fBas ` Y ) <-> ( F C_ ~P Y /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
10 9 3ad2ant3 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> ( F e. ( fBas ` Y ) <-> ( F C_ ~P Y /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
11 1 8 10 mpbir2and 
 |-  ( ( F e. ( fBas ` X ) /\ F C_ ~P Y /\ Y e. V ) -> F e. ( fBas ` Y ) )