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