Step |
Hyp |
Ref |
Expression |
1 |
|
frlmfielbas.f |
|- F = ( R freeLMod I ) |
2 |
|
frlmfielbas.n |
|- N = ( Base ` R ) |
3 |
|
frlmfielbas.b |
|- B = ( Base ` F ) |
4 |
3
|
eleq2i |
|- ( X e. B <-> X e. ( Base ` F ) ) |
5 |
1 2
|
frlmfibas |
|- ( ( R e. V /\ I e. Fin ) -> ( N ^m I ) = ( Base ` F ) ) |
6 |
5
|
eleq2d |
|- ( ( R e. V /\ I e. Fin ) -> ( X e. ( N ^m I ) <-> X e. ( Base ` F ) ) ) |
7 |
2
|
fvexi |
|- N e. _V |
8 |
7
|
a1i |
|- ( ( R e. V /\ I e. Fin ) -> N e. _V ) |
9 |
|
simpr |
|- ( ( R e. V /\ I e. Fin ) -> I e. Fin ) |
10 |
8 9
|
elmapd |
|- ( ( R e. V /\ I e. Fin ) -> ( X e. ( N ^m I ) <-> X : I --> N ) ) |
11 |
6 10
|
bitr3d |
|- ( ( R e. V /\ I e. Fin ) -> ( X e. ( Base ` F ) <-> X : I --> N ) ) |
12 |
4 11
|
syl5bb |
|- ( ( R e. V /\ I e. Fin ) -> ( X e. B <-> X : I --> N ) ) |