Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-lmic | Structured version Visualization version GIF version |
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 |
---|---|
df-lmic | ⊢ ≃𝑚 = (◡ LMIso “ (V ∖ 1o)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clmic 20271 | . 2 class ≃𝑚 | |
2 | clmim 20270 | . . . 4 class LMIso | |
3 | 2 | ccnv 5584 | . . 3 class ◡ LMIso |
4 | cvv 3430 | . . . 4 class V | |
5 | c1o 8278 | . . . 4 class 1o | |
6 | 4, 5 | cdif 3884 | . . 3 class (V ∖ 1o) |
7 | 3, 6 | cima 5588 | . 2 class (◡ LMIso “ (V ∖ 1o)) |
8 | 1, 7 | wceq 1539 | 1 wff ≃𝑚 = (◡ LMIso “ (V ∖ 1o)) |
Colors of variables: wff setvar class |
This definition is referenced by: brlmic 20318 |
Copyright terms: Public domain | W3C validator |