Theorem lmimfn

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

	Ref	Expression
Assertion	lmimfn	⊢ LMIso Fn ( LMod × LMod )

Proof

Step	Hyp	Ref	Expression
1		df-lmim	⊢ LMIso = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )
2		ovex	⊢ ( 𝑠 LMHom 𝑡 ) ∈ V
3	2	rabex	⊢ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } ∈ V
4	1 3	fnmpoi	⊢ LMIso Fn ( LMod × LMod )