Description: Define the set of ring isomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-rngiso | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crs | |
|
1 | vr | |
|
2 | cvv | |
|
3 | vs | |
|
4 | vf | |
|
5 | 1 | cv | |
6 | crh | |
|
7 | 3 | cv | |
8 | 5 7 6 | co | |
9 | 4 | cv | |
10 | 9 | ccnv | |
11 | 7 5 6 | co | |
12 | 10 11 | wcel | |
13 | 12 4 8 | crab | |
14 | 1 3 2 2 13 | cmpo | |
15 | 0 14 | wceq | |