Step |
Hyp |
Ref |
Expression |
1 |
|
fbasne0 |
|- ( F e. ( fBas ` B ) -> F =/= (/) ) |
2 |
|
n0 |
|- ( F =/= (/) <-> E. x x e. F ) |
3 |
1 2
|
sylib |
|- ( F e. ( fBas ` B ) -> E. x x e. F ) |
4 |
|
ssv |
|- x C_ _V |
5 |
4
|
jctr |
|- ( x e. F -> ( x e. F /\ x C_ _V ) ) |
6 |
5
|
eximi |
|- ( E. x x e. F -> E. x ( x e. F /\ x C_ _V ) ) |
7 |
|
df-rex |
|- ( E. x e. F x C_ _V <-> E. x ( x e. F /\ x C_ _V ) ) |
8 |
6 7
|
sylibr |
|- ( E. x x e. F -> E. x e. F x C_ _V ) |
9 |
3 8
|
syl |
|- ( F e. ( fBas ` B ) -> E. x e. F x C_ _V ) |
10 |
|
inteq |
|- ( A = (/) -> |^| A = |^| (/) ) |
11 |
|
int0 |
|- |^| (/) = _V |
12 |
10 11
|
eqtrdi |
|- ( A = (/) -> |^| A = _V ) |
13 |
12
|
sseq2d |
|- ( A = (/) -> ( x C_ |^| A <-> x C_ _V ) ) |
14 |
13
|
rexbidv |
|- ( A = (/) -> ( E. x e. F x C_ |^| A <-> E. x e. F x C_ _V ) ) |
15 |
9 14
|
syl5ibrcom |
|- ( F e. ( fBas ` B ) -> ( A = (/) -> E. x e. F x C_ |^| A ) ) |
16 |
15
|
3ad2ant1 |
|- ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) -> ( A = (/) -> E. x e. F x C_ |^| A ) ) |
17 |
|
simpl1 |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> F e. ( fBas ` B ) ) |
18 |
|
simpl2 |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> A C_ F ) |
19 |
|
simpr |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> A =/= (/) ) |
20 |
|
simpl3 |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> A e. Fin ) |
21 |
|
elfir |
|- ( ( F e. ( fBas ` B ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. ( fi ` F ) ) |
22 |
17 18 19 20 21
|
syl13anc |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> |^| A e. ( fi ` F ) ) |
23 |
|
fbssfi |
|- ( ( F e. ( fBas ` B ) /\ |^| A e. ( fi ` F ) ) -> E. x e. F x C_ |^| A ) |
24 |
17 22 23
|
syl2anc |
|- ( ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) /\ A =/= (/) ) -> E. x e. F x C_ |^| A ) |
25 |
24
|
ex |
|- ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) -> ( A =/= (/) -> E. x e. F x C_ |^| A ) ) |
26 |
16 25
|
pm2.61dne |
|- ( ( F e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) -> E. x e. F x C_ |^| A ) |