Metamath Proof Explorer

Theorem lmimfn

Description: Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion lmimfn 
|- LMIso Fn ( LMod X. LMod )

Proof

Step Hyp Ref Expression
1 df-lmim 
 |-  LMIso = ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
2 ovex 
 |-  ( s LMHom t ) e. _V
3 2 rabex 
 |-  { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } e. _V
4 1 3 fnmpoi 
 |-  LMIso Fn ( LMod X. LMod )