Step |
Hyp |
Ref |
Expression |
1 |
|
mdet0pr |
|- ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } ) |
2 |
|
0ex |
|- (/) e. _V |
3 |
|
fvex |
|- ( 1r ` R ) e. _V |
4 |
2 3
|
f1osn |
|- { <. (/) , ( 1r ` R ) >. } : { (/) } -1-1-onto-> { ( 1r ` R ) } |
5 |
|
f1oeq1 |
|- ( ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } -> ( ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } <-> { <. (/) , ( 1r ` R ) >. } : { (/) } -1-1-onto-> { ( 1r ` R ) } ) ) |
6 |
4 5
|
mpbiri |
|- ( ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } -> ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } ) |
7 |
1 6
|
syl |
|- ( R e. Ring -> ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } ) |