Metamath Proof Explorer

Theorem oppcup

Description: The universal pair <. X , M >. from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses oppcup.b 
|- B = ( Base ` D )
oppcup.c 
|- C = ( Base ` E )
oppcup.h 
|- H = ( Hom ` D )
oppcup.j 
|- J = ( Hom ` E )
oppcup.xb 
|- .xb = ( comp ` E )
oppcup.w 
|- ( ph -> W e. C )
oppcup.f 
|- ( ph -> F ( D Func E ) G )
oppcup.x 
|- ( ph -> X e. B )
oppcup.m 
|- ( ph -> M e. ( ( F ` X ) J W ) )
oppcup.o 
|- O = ( oppCat ` D )
oppcup.p 
|- P = ( oppCat ` E )
Assertion oppcup 
|- ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 oppcup.b 
 |-  B = ( Base ` D )
2 oppcup.c 
 |-  C = ( Base ` E )
3 oppcup.h 
 |-  H = ( Hom ` D )
4 oppcup.j 
 |-  J = ( Hom ` E )
5 oppcup.xb 
 |-  .xb = ( comp ` E )
6 oppcup.w 
 |-  ( ph -> W e. C )
7 oppcup.f 
 |-  ( ph -> F ( D Func E ) G )
8 oppcup.x 
 |-  ( ph -> X e. B )
9 oppcup.m 
 |-  ( ph -> M e. ( ( F ` X ) J W ) )
10 oppcup.o 
 |-  O = ( oppCat ` D )
11 oppcup.p 
 |-  P = ( oppCat ` E )
12 10 1 oppcbas 
 |-  B = ( Base ` O )
13 11 2 oppcbas 
 |-  C = ( Base ` P )
14 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
15 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
16 eqid 
 |-  ( comp ` P ) = ( comp ` P )
17 10 11 7 funcoppc 
 |-  ( ph -> F ( O Func P ) tpos G )
18 4 11 oppchom 
 |-  ( W ( Hom ` P ) ( F ` X ) ) = ( ( F ` X ) J W )
19 9 18 eleqtrrdi 
 |-  ( ph -> M e. ( W ( Hom ` P ) ( F ` X ) ) )
20 12 13 14 15 16 6 17 8 19 isup 
 |-  ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( W ( Hom ` P ) ( F ` y ) ) E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) ) )
21 4 11 oppchom 
 |-  ( W ( Hom ` P ) ( F ` y ) ) = ( ( F ` y ) J W )
22 21 a1i 
 |-  ( ( ph /\ y e. B ) -> ( W ( Hom ` P ) ( F ` y ) ) = ( ( F ` y ) J W ) )
23 3 10 oppchom 
 |-  ( X ( Hom ` O ) y ) = ( y H X )
24 23 a1i 
 |-  ( ( ph /\ y e. B ) -> ( X ( Hom ` O ) y ) = ( y H X ) )
25 ovtpos 
 |-  ( X tpos G y ) = ( y G X )
26 25 fveq1i 
 |-  ( ( X tpos G y ) ` k ) = ( ( y G X ) ` k )
27 26 oveq1i 
 |-  ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) = ( ( ( y G X ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M )
28 6 adantr 
 |-  ( ( ph /\ y e. B ) -> W e. C )
29 7 adantr 
 |-  ( ( ph /\ y e. B ) -> F ( D Func E ) G )
30 1 2 29 funcf1 
 |-  ( ( ph /\ y e. B ) -> F : B --> C )
31 8 adantr 
 |-  ( ( ph /\ y e. B ) -> X e. B )
32 30 31 ffvelcdmd 
 |-  ( ( ph /\ y e. B ) -> ( F ` X ) e. C )
33 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
34 30 33 ffvelcdmd 
 |-  ( ( ph /\ y e. B ) -> ( F ` y ) e. C )
35 2 5 11 28 32 34 oppcco 
 |-  ( ( ph /\ y e. B ) -> ( ( ( y G X ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) )
36 27 35 eqtrid 
 |-  ( ( ph /\ y e. B ) -> ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) )
37 36 eqeq2d 
 |-  ( ( ph /\ y e. B ) -> ( g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) <-> g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )
38 24 37 reueqbidv 
 |-  ( ( ph /\ y e. B ) -> ( E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) <-> E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )
39 22 38 raleqbidv 
 |-  ( ( ph /\ y e. B ) -> ( A. g e. ( W ( Hom ` P ) ( F ` y ) ) E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) <-> A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )
40 39 ralbidva 
 |-  ( ph -> ( A. y e. B A. g e. ( W ( Hom ` P ) ( F ` y ) ) E! k e. ( X ( Hom ` O ) y ) g = ( ( ( X tpos G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` P ) ( F ` y ) ) M ) <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )
41 20 40 bitrd 
 |-  ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) )