Definition df-lmic

Description: Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	df-lmic	$$⊢{\simeq }_{𝑚}={\mathrm{LMIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmic	$$class{\simeq }_{𝑚}$$
1		clmim	$$class\mathrm{LMIso}$$
2	1	ccnv	$$class{\mathrm{LMIso}}^{-1}$$
3		cvv	$$class\mathrm{V}$$
4		c1o	$$class{1}_{𝑜}$$
5	3 4	cdif	$$class\left(\mathrm{V}\setminus 1_{𝑜}\right)$$
6	2 5	cima	$$class{\mathrm{LMIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
7	0 6	wceq	$$wff{\simeq }_{𝑚}={\mathrm{LMIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$