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

Metamath Proof Explorer

Theorem upeu3

Description: The universal pair <. X , M >. from object W to functor <. F , G >. is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses upeu3.i 
|- ( ph -> I = ( Iso ` D ) )
upeu3.o 
|- ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) )
upeu3.x 
|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
upeu3.y 
|- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N )
Assertion upeu3 
|- ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) )

Proof

Step Hyp Ref Expression
1 upeu3.i 
 |-  ( ph -> I = ( Iso ` D ) )
2 upeu3.o 
 |-  ( ph -> .o. = ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) )
3 upeu3.x 
 |-  ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
4 upeu3.y 
 |-  ( ph -> Y ( <. F , G >. ( D UP E ) W ) N )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 eqid 
 |-  ( Base ` E ) = ( Base ` E )
7 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
8 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
9 eqid 
 |-  ( comp ` E ) = ( comp ` E )
10 3 uprcl2 
 |-  ( ph -> F ( D Func E ) G )
11 3 5 uprcl4 
 |-  ( ph -> X e. ( Base ` D ) )
12 4 5 uprcl4 
 |-  ( ph -> Y e. ( Base ` D ) )
13 3 6 uprcl3 
 |-  ( ph -> W e. ( Base ` E ) )
14 3 8 uprcl5 
 |-  ( ph -> M e. ( W ( Hom ` E ) ( F ` X ) ) )
15 5 7 8 9 3 isup2 
 |-  ( ph -> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( X ( Hom ` D ) y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` y ) ) M ) )
16 4 8 uprcl5 
 |-  ( ph -> N e. ( W ( Hom ` E ) ( F ` Y ) ) )
17 5 7 8 9 4 isup2 
 |-  ( ph -> A. y e. ( Base ` D ) A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( Y ( Hom ` D ) y ) g = ( ( ( Y G y ) ` k ) ( <. W , ( F ` Y ) >. ( comp ` E ) ( F ` y ) ) N ) )
18 5 6 7 8 9 10 11 12 13 14 15 16 17 upeu 
 |-  ( ph -> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) )
19 1 oveqd 
 |-  ( ph -> ( X I Y ) = ( X ( Iso ` D ) Y ) )
20 2 oveqd 
 |-  ( ph -> ( ( ( X G Y ) ` r ) .o. M ) = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) )
21 20 eqeq2d 
 |-  ( ph -> ( N = ( ( ( X G Y ) ` r ) .o. M ) <-> N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) )
22 19 21 reueqbidv 
 |-  ( ph -> ( E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) <-> E! r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) ) )
23 18 22 mpbird 
 |-  ( ph -> E! r e. ( X I Y ) N = ( ( ( X G Y ) ` r ) .o. M ) )