Theorem brlmici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	brlmici	$$⊢F\in \left(R\mathrm{LMIso}S\right)\to R{\simeq }_{𝑚}S$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢F\in \left(R\mathrm{LMIso}S\right)\to R\mathrm{LMIso}S\ne \varnothing$$
2		brlmic	$$⊢R{\simeq }_{𝑚}S\leftrightarrow R\mathrm{LMIso}S\ne \varnothing$$
3	1 2	sylibr	$$⊢F\in \left(R\mathrm{LMIso}S\right)\to R{\simeq }_{𝑚}S$$