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