Metamath Proof Explorer

Theorem upeu4

Description: Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-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 )
upeu4.k 
|- ( ph -> K e. ( X I Y ) )
upeu4.n 
|- ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) )
Assertion upeu4 
|- ( ph -> Y ( <. F , G >. ( D UP E ) W ) N )

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 upeu4.k 
 |-  ( ph -> K e. ( X I Y ) )
5 upeu4.n 
 |-  ( ph -> N = ( ( ( X G Y ) ` K ) .o. M ) )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
10 eqid 
 |-  ( comp ` E ) = ( comp ` E )
11 3 uprcl2 
 |-  ( ph -> F ( D Func E ) G )
12 3 6 uprcl4 
 |-  ( ph -> X e. ( Base ` D ) )
13 11 funcrcl2 
 |-  ( ph -> D e. Cat )
14 isofn 
 |-  ( D e. Cat -> ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
15 13 14 syl 
 |-  ( ph -> ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
16 1 fneq1d 
 |-  ( ph -> ( I Fn ( ( Base ` D ) X. ( Base ` D ) ) <-> ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) ) )
17 15 16 mpbird 
 |-  ( ph -> I Fn ( ( Base ` D ) X. ( Base ` D ) ) )
18 fnov 
 |-  ( I Fn ( ( Base ` D ) X. ( Base ` D ) ) <-> I = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) )
19 17 18 sylib 
 |-  ( ph -> I = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) )
20 19 oveqd 
 |-  ( ph -> ( X I Y ) = ( X ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) Y ) )
21 4 20 eleqtrd 
 |-  ( ph -> K e. ( X ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) Y ) )
22 eqid 
 |-  ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) )
23 22 elmpocl2 
 |-  ( K e. ( X ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x I y ) ) Y ) -> Y e. ( Base ` D ) )
24 21 23 syl 
 |-  ( ph -> Y e. ( Base ` D ) )
25 3 7 uprcl3 
 |-  ( ph -> W e. ( Base ` E ) )
26 3 9 uprcl5 
 |-  ( ph -> M e. ( W ( Hom ` E ) ( F ` X ) ) )
27 6 8 9 10 3 isup2 
 |-  ( ph -> A. x e. ( Base ` D ) A. f e. ( W ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` D ) x ) f = ( ( ( X G x ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) )
28 eqid 
 |-  ( Iso ` D ) = ( Iso ` D )
29 1 oveqd 
 |-  ( ph -> ( X I Y ) = ( X ( Iso ` D ) Y ) )
30 4 29 eleqtrd 
 |-  ( ph -> K e. ( X ( Iso ` D ) Y ) )
31 2 oveqd 
 |-  ( ph -> ( ( ( X G Y ) ` K ) .o. M ) = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) )
32 5 31 eqtrd 
 |-  ( ph -> N = ( ( ( X G Y ) ` K ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` Y ) ) M ) )
33 6 7 8 9 10 11 12 24 25 26 27 28 30 32 upeu2 
 |-  ( ph -> ( N e. ( W ( Hom ` E ) ( F ` Y ) ) /\ 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 ) ) )
34 33 simprd 
 |-  ( 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 ) )
35 33 simpld 
 |-  ( ph -> N e. ( W ( Hom ` E ) ( F ` Y ) ) )
36 6 7 8 9 10 25 11 24 35 isup 
 |-  ( ph -> ( Y ( <. F , G >. ( D UP E ) W ) N <-> 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 ) ) )
37 34 36 mpbird 
 |-  ( ph -> Y ( <. F , G >. ( D UP E ) W ) N )