Theorem lmimfn

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

	Ref	Expression
Assertion	lmimfn	$$⊢\mathrm{LMIso}Fn\left(\mathrm{LMod}\times \mathrm{LMod}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-lmim	$$⊢\mathrm{LMIso}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$
2		ovex	$$⊢s\mathrm{LMHom}t\in \mathrm{V}$$
3	2	rabex	$$⊢\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\in \mathrm{V}$$
4	1 3	fnmpoi	$$⊢\mathrm{LMIso}Fn\left(\mathrm{LMod}\times \mathrm{LMod}\right)$$