Step |
Hyp |
Ref |
Expression |
1 |
|
funcringcsetcALTV.r |
|- R = ( RingCatALTV ` U ) |
2 |
|
funcringcsetcALTV.s |
|- S = ( SetCat ` U ) |
3 |
|
funcringcsetcALTV.b |
|- B = ( Base ` R ) |
4 |
|
funcringcsetcALTV.c |
|- C = ( Base ` S ) |
5 |
|
funcringcsetcALTV.u |
|- ( ph -> U e. WUni ) |
6 |
|
funcringcsetcALTV.f |
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
7 |
|
funcringcsetcALTV.g |
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) ) |
8 |
1 2 3 4 5 6 7
|
funcringcsetclem5ALTV |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) ) |
9 |
8
|
3adant3 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) ) |
10 |
9
|
fveq1d |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = ( ( _I |` ( X RingHom Y ) ) ` H ) ) |
11 |
|
fvresi |
|- ( H e. ( X RingHom Y ) -> ( ( _I |` ( X RingHom Y ) ) ` H ) = H ) |
12 |
11
|
3ad2ant3 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( _I |` ( X RingHom Y ) ) ` H ) = H ) |
13 |
10 12
|
eqtrd |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H ) |