Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
|- ( F e. ( fBas ` B ) -> B e. dom fBas ) |
2 |
|
isfbas |
|- ( B e. dom fBas -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
3 |
1 2
|
syl |
|- ( F e. ( fBas ` B ) -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
4 |
3
|
ibi |
|- ( F e. ( fBas ` B ) -> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) |
5 |
|
simpr1 |
|- ( ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) -> F =/= (/) ) |
6 |
4 5
|
syl |
|- ( F e. ( fBas ` B ) -> F =/= (/) ) |