Metamath Proof Explorer

Theorem upfval3

Description: Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses upfval.b 
|- B = ( Base ` D )
upfval.c 
|- C = ( Base ` E )
upfval.h 
|- H = ( Hom ` D )
upfval.j 
|- J = ( Hom ` E )
upfval.o 
|- O = ( comp ` E )
upfval2.w 
|- ( ph -> W e. C )
upfval3.f 
|- ( ph -> F ( D Func E ) G )
Assertion upfval3 
|- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } )

Proof

Step Hyp Ref Expression
1 upfval.b 
 |-  B = ( Base ` D )
2 upfval.c 
 |-  C = ( Base ` E )
3 upfval.h 
 |-  H = ( Hom ` D )
4 upfval.j 
 |-  J = ( Hom ` E )
5 upfval.o 
 |-  O = ( comp ` E )
6 upfval2.w 
 |-  ( ph -> W e. C )
7 upfval3.f 
 |-  ( ph -> F ( D Func E ) G )
8 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
9 7 8 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
10 1 2 3 4 5 6 9 upfval2 
 |-  ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) } )
11 relfunc 
 |-  Rel ( D Func E )
12 11 brrelex12i 
 |-  ( F ( D Func E ) G -> ( F e. _V /\ G e. _V ) )
13 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
14 12 13 syl 
 |-  ( F ( D Func E ) G -> ( 1st ` <. F , G >. ) = F )
15 14 fveq1d 
 |-  ( F ( D Func E ) G -> ( ( 1st ` <. F , G >. ) ` x ) = ( F ` x ) )
16 15 oveq2d 
 |-  ( F ( D Func E ) G -> ( W J ( ( 1st ` <. F , G >. ) ` x ) ) = ( W J ( F ` x ) ) )
17 16 eleq2d 
 |-  ( F ( D Func E ) G -> ( m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) <-> m e. ( W J ( F ` x ) ) ) )
18 17 anbi2d 
 |-  ( F ( D Func E ) G -> ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) <-> ( x e. B /\ m e. ( W J ( F ` x ) ) ) ) )
19 14 fveq1d 
 |-  ( F ( D Func E ) G -> ( ( 1st ` <. F , G >. ) ` y ) = ( F ` y ) )
20 19 oveq2d 
 |-  ( F ( D Func E ) G -> ( W J ( ( 1st ` <. F , G >. ) ` y ) ) = ( W J ( F ` y ) ) )
21 15 opeq2d 
 |-  ( F ( D Func E ) G -> <. W , ( ( 1st ` <. F , G >. ) ` x ) >. = <. W , ( F ` x ) >. )
22 21 19 oveq12d 
 |-  ( F ( D Func E ) G -> ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) = ( <. W , ( F ` x ) >. O ( F ` y ) ) )
23 op2ndg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 2nd ` <. F , G >. ) = G )
24 12 23 syl 
 |-  ( F ( D Func E ) G -> ( 2nd ` <. F , G >. ) = G )
25 24 oveqd 
 |-  ( F ( D Func E ) G -> ( x ( 2nd ` <. F , G >. ) y ) = ( x G y ) )
26 25 fveq1d 
 |-  ( F ( D Func E ) G -> ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) = ( ( x G y ) ` k ) )
27 eqidd 
 |-  ( F ( D Func E ) G -> m = m )
28 22 26 27 oveq123d 
 |-  ( F ( D Func E ) G -> ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) )
29 28 eqeq2d 
 |-  ( F ( D Func E ) G -> ( g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) <-> g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) )
30 29 reubidv 
 |-  ( F ( D Func E ) G -> ( E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) <-> E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) )
31 20 30 raleqbidv 
 |-  ( F ( D Func E ) G -> ( A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) <-> A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) )
32 31 ralbidv 
 |-  ( F ( D Func E ) G -> ( A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) )
33 18 32 anbi12d 
 |-  ( F ( D Func E ) G -> ( ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) <-> ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) ) )
34 33 opabbidv 
 |-  ( F ( D Func E ) G -> { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } )
35 7 34 syl 
 |-  ( ph -> { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } )
36 10 35 eqtrd 
 |-  ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } )