| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-ric |
|- ~=r = ( `' RingIso " ( _V \ 1o ) ) |
| 2 |
|
ovex |
|- ( r RingHom s ) e. _V |
| 3 |
|
rabexg |
|- ( ( r RingHom s ) e. _V -> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V ) |
| 4 |
2 3
|
mp1i |
|- ( ( r e. _V /\ s e. _V ) -> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V ) |
| 5 |
4
|
rgen2 |
|- A. r e. _V A. s e. _V { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V |
| 6 |
|
df-rim |
|- RingIso = ( r e. _V , s e. _V |-> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } ) |
| 7 |
6
|
fnmpo |
|- ( A. r e. _V A. s e. _V { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V -> RingIso Fn ( _V X. _V ) ) |
| 8 |
5 7
|
ax-mp |
|- RingIso Fn ( _V X. _V ) |
| 9 |
1 8
|
brwitnlem |
|- ( R ~=r S <-> ( R RingIso S ) =/= (/) ) |