Step |
Hyp |
Ref |
Expression |
1 |
|
deg1fval.d |
|- D = ( deg1 ` R ) |
2 |
|
oveq2 |
|- ( r = R -> ( 1o mDeg r ) = ( 1o mDeg R ) ) |
3 |
|
df-deg1 |
|- deg1 = ( r e. _V |-> ( 1o mDeg r ) ) |
4 |
|
ovex |
|- ( 1o mDeg R ) e. _V |
5 |
2 3 4
|
fvmpt |
|- ( R e. _V -> ( deg1 ` R ) = ( 1o mDeg R ) ) |
6 |
|
fvprc |
|- ( -. R e. _V -> ( deg1 ` R ) = (/) ) |
7 |
|
reldmmdeg |
|- Rel dom mDeg |
8 |
7
|
ovprc2 |
|- ( -. R e. _V -> ( 1o mDeg R ) = (/) ) |
9 |
6 8
|
eqtr4d |
|- ( -. R e. _V -> ( deg1 ` R ) = ( 1o mDeg R ) ) |
10 |
5 9
|
pm2.61i |
|- ( deg1 ` R ) = ( 1o mDeg R ) |
11 |
1 10
|
eqtri |
|- D = ( 1o mDeg R ) |