This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppcup3

Description: The universal property for the universal pair <. X , M >. from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses oppcup3.b 
|- B = ( Base ` D )
oppcup3.h 
|- H = ( Hom ` D )
oppcup3.j 
|- J = ( Hom ` E )
oppcup3.xb 
|- .xb = ( comp ` E )
oppcup3.o 
|- O = ( oppCat ` D )
oppcup3.p 
|- P = ( oppCat ` E )
oppcup3.x 
|- ( ph -> X ( <. F , T >. ( O UP P ) W ) M )
oppcup3.g 
|- ( ph -> tpos T = G )
oppcup3.y 
|- ( ph -> Y e. B )
oppcup3.n 
|- ( ph -> N e. ( ( F ` Y ) J W ) )
Assertion oppcup3 
|- ( ph -> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. .xb W ) ( ( Y G X ) ` k ) ) )

Proof

Step Hyp Ref Expression
1 oppcup3.b 
 |-  B = ( Base ` D )
2 oppcup3.h 
 |-  H = ( Hom ` D )
3 oppcup3.j 
 |-  J = ( Hom ` E )
4 oppcup3.xb 
 |-  .xb = ( comp ` E )
5 oppcup3.o 
 |-  O = ( oppCat ` D )
6 oppcup3.p 
 |-  P = ( oppCat ` E )
7 oppcup3.x 
 |-  ( ph -> X ( <. F , T >. ( O UP P ) W ) M )
8 oppcup3.g 
 |-  ( ph -> tpos T = G )
9 oppcup3.y 
 |-  ( ph -> Y e. B )
10 oppcup3.n 
 |-  ( ph -> N e. ( ( F ` Y ) J W ) )
11 9 1 eleqtrdi 
 |-  ( ph -> Y e. ( Base ` D ) )
12 11 elfvexd 
 |-  ( ph -> D e. _V )
13 10 ne0d 
 |-  ( ph -> ( ( F ` Y ) J W ) =/= (/) )
14 fvprc 
 |-  ( -. E e. _V -> ( Hom ` E ) = (/) )
15 3 14 eqtrid 
 |-  ( -. E e. _V -> J = (/) )
16 15 oveqd 
 |-  ( -. E e. _V -> ( ( F ` Y ) J W ) = ( ( F ` Y ) (/) W ) )
17 0ov 
 |-  ( ( F ` Y ) (/) W ) = (/)
18 16 17 eqtrdi 
 |-  ( -. E e. _V -> ( ( F ` Y ) J W ) = (/) )
19 18 necon1ai 
 |-  ( ( ( F ` Y ) J W ) =/= (/) -> E e. _V )
20 13 19 syl 
 |-  ( ph -> E e. _V )
21 7 6 5 12 20 8 oppcuprcl2 
 |-  ( ph -> F ( D Func E ) G )
22 7 8 uptpos 
 |-  ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M )
23 1 2 3 4 5 6 21 22 oppcup2 
 |-  ( ph -> 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 ) ) )
24 23 9 10 oppcup3lem 
 |-  ( ph -> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. .xb W ) ( ( Y G X ) ` k ) ) )