Metamath Proof Explorer

Theorem oppc1stf

Description: The opposite functor of the first projection functor is the first projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025)

Ref Expression
Hypotheses oppc1stf.o 
|- O = ( oppCat ` C )
oppc1stf.p 
|- P = ( oppCat ` D )
oppc1stf.c 
|- ( ph -> C e. V )
oppc1stf.d 
|- ( ph -> D e. W )
Assertion oppc1stf 
|- ( ph -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) )

Proof

Step Hyp Ref Expression
1 oppc1stf.o 
 |-  O = ( oppCat ` C )
2 oppc1stf.p 
 |-  P = ( oppCat ` D )
3 oppc1stf.c 
 |-  ( ph -> C e. V )
4 oppc1stf.d 
 |-  ( ph -> D e. W )
5 eqid 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) )
6 5 tposmpo 
 |-  tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) = ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 7 1 oppchom 
 |-  ( ( 1st ` y ) ( Hom ` O ) ( 1st ` x ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 9 2 oppchom 
 |-  ( ( 2nd ` y ) ( Hom ` P ) ( 2nd ` x ) ) = ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) )
11 8 10 xpeq12i 
 |-  ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` x ) ) X. ( ( 2nd ` y ) ( Hom ` P ) ( 2nd ` x ) ) ) = ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) )
12 eqid 
 |-  ( O Xc. P ) = ( O Xc. P )
13 eqid 
 |-  ( Base ` C ) = ( Base ` C )
14 1 13 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 2 15 oppcbas 
 |-  ( Base ` D ) = ( Base ` P )
17 12 14 16 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( O Xc. P ) )
18 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
19 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
20 eqid 
 |-  ( Hom ` ( O Xc. P ) ) = ( Hom ` ( O Xc. P ) )
21 simp2 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` D ) ) )
22 simp3 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` D ) ) )
23 12 17 18 19 20 21 22 xpchom 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( y ( Hom ` ( O Xc. P ) ) x ) = ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` x ) ) X. ( ( 2nd ` y ) ( Hom ` P ) ( 2nd ` x ) ) ) )
24 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
25 24 13 15 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C Xc. D ) )
26 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
27 24 25 7 9 26 22 21 xpchom 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( x ( Hom ` ( C Xc. D ) ) y ) = ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) )
28 11 23 27 3eqtr4a 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( y ( Hom ` ( O Xc. P ) ) x ) = ( x ( Hom ` ( C Xc. D ) ) y ) )
29 28 reseq2d 
 |-  ( ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( 1st |` ( y ( Hom ` ( O Xc. P ) ) x ) ) = ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) )
30 29 mpoeq3dva 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( y ( Hom ` ( O Xc. P ) ) x ) ) ) = ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) )
31 6 30 eqtr4id 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) = ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( y ( Hom ` ( O Xc. P ) ) x ) ) ) )
32 31 opeq2d 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) >. = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( y ( Hom ` ( O Xc. P ) ) x ) ) ) >. )
33 simprl 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> C e. Cat )
34 simprr 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> D e. Cat )
35 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
36 24 25 26 33 34 35 1stfval 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( C 1stF D ) = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) >. )
37 24 33 34 35 1stfcl 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
38 36 37 oppfval3 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) >. )
39 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
40 33 39 syl 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> O e. Cat )
41 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
42 34 41 syl 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> P e. Cat )
43 eqid 
 |-  ( O 1stF P ) = ( O 1stF P )
44 12 17 20 40 42 43 1stfval 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( O 1stF P ) = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( y e. ( ( Base ` C ) X. ( Base ` D ) ) , x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( y ( Hom ` ( O Xc. P ) ) x ) ) ) >. )
45 32 38 44 3eqtr4d 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) )
46 df-1stf 
 |-  1stF = ( c e. Cat , d e. Cat |-> [_ ( ( Base ` c ) X. ( Base ` d ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( c Xc. d ) ) y ) ) ) >. )
47 1 2 3 4 45 46 oppc1stflem 
 |-  ( ph -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) )