| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fucoppclem.o |
|- O = ( oppCat ` C ) |
| 2 |
|
fucoppclem.p |
|- P = ( oppCat ` D ) |
| 3 |
|
fucoppclem.n |
|- N = ( C Nat D ) |
| 4 |
|
fucoppclem.f |
|- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) |
| 5 |
|
fucoppclem.x |
|- ( ph -> X e. ( C Func D ) ) |
| 6 |
|
fucoppclem.y |
|- ( ph -> Y e. ( C Func D ) ) |
| 7 |
|
eqid |
|- ( O Nat P ) = ( O Nat P ) |
| 8 |
4
|
fveq1d |
|- ( ph -> ( F ` Y ) = ( ( oppFunc |` ( C Func D ) ) ` Y ) ) |
| 9 |
6
|
fvresd |
|- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` Y ) = ( oppFunc ` Y ) ) |
| 10 |
8 9
|
eqtrd |
|- ( ph -> ( F ` Y ) = ( oppFunc ` Y ) ) |
| 11 |
4
|
fveq1d |
|- ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) ) |
| 12 |
5
|
fvresd |
|- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) ) |
| 13 |
11 12
|
eqtrd |
|- ( ph -> ( F ` X ) = ( oppFunc ` X ) ) |
| 14 |
5
|
func1st2nd |
|- ( ph -> ( 1st ` X ) ( C Func D ) ( 2nd ` X ) ) |
| 15 |
14
|
funcrcl2 |
|- ( ph -> C e. Cat ) |
| 16 |
14
|
funcrcl3 |
|- ( ph -> D e. Cat ) |
| 17 |
1 2 3 7 10 13 15 16
|
natoppfb |
|- ( ph -> ( Y N X ) = ( ( F ` X ) ( O Nat P ) ( F ` Y ) ) ) |