Metamath Proof Explorer

Theorem upfval2

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 )
upfval2.f 
|- ( ph -> F e. ( D Func E ) )
Assertion upfval2 
|- ( ph -> ( F ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` 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 upfval2.f 
 |-  ( ph -> F e. ( D Func E ) )
8 anass 
 |-  ( ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) <-> ( x e. B /\ ( m e. ( W J ( ( 1st ` F ) ` x ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) )
9 8 opabbii 
 |-  { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } = { <. x , m >. | ( x e. B /\ ( m e. ( W J ( ( 1st ` F ) ` x ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) }
10 1 fvexi 
 |-  B e. _V
11 10 a1i 
 |-  ( ph -> B e. _V )
12 simprl 
 |-  ( ( ( ph /\ x e. B ) /\ ( m e. ( W J ( ( 1st ` F ) ` x ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) -> m e. ( W J ( ( 1st ` F ) ` x ) ) )
13 ovexd 
 |-  ( ( ph /\ x e. B ) -> ( W J ( ( 1st ` F ) ` x ) ) e. _V )
14 12 13 abexd 
 |-  ( ( ph /\ x e. B ) -> { m | ( m e. ( W J ( ( 1st ` F ) ` x ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } e. _V )
15 11 14 opabex3d 
 |-  ( ph -> { <. x , m >. | ( x e. B /\ ( m e. ( W J ( ( 1st ` F ) ` x ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) } e. _V )
16 9 15 eqeltrid 
 |-  ( ph -> { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } e. _V )
17 fveq2 
 |-  ( f = F -> ( 1st ` f ) = ( 1st ` F ) )
18 17 fveq1d 
 |-  ( f = F -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` x ) )
19 18 oveq2d 
 |-  ( f = F -> ( w J ( ( 1st ` f ) ` x ) ) = ( w J ( ( 1st ` F ) ` x ) ) )
20 19 eleq2d 
 |-  ( f = F -> ( m e. ( w J ( ( 1st ` f ) ` x ) ) <-> m e. ( w J ( ( 1st ` F ) ` x ) ) ) )
21 20 anbi2d 
 |-  ( f = F -> ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) <-> ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) ) )
22 17 fveq1d 
 |-  ( f = F -> ( ( 1st ` f ) ` y ) = ( ( 1st ` F ) ` y ) )
23 22 oveq2d 
 |-  ( f = F -> ( w J ( ( 1st ` f ) ` y ) ) = ( w J ( ( 1st ` F ) ` y ) ) )
24 18 opeq2d 
 |-  ( f = F -> <. w , ( ( 1st ` f ) ` x ) >. = <. w , ( ( 1st ` F ) ` x ) >. )
25 24 22 oveq12d 
 |-  ( f = F -> ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) = ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) )
26 fveq2 
 |-  ( f = F -> ( 2nd ` f ) = ( 2nd ` F ) )
27 26 oveqd 
 |-  ( f = F -> ( x ( 2nd ` f ) y ) = ( x ( 2nd ` F ) y ) )
28 27 fveq1d 
 |-  ( f = F -> ( ( x ( 2nd ` f ) y ) ` k ) = ( ( x ( 2nd ` F ) y ) ` k ) )
29 eqidd 
 |-  ( f = F -> m = m )
30 25 28 29 oveq123d 
 |-  ( f = F -> ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) )
31 30 eqeq2d 
 |-  ( f = F -> ( g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) <-> g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
32 31 reubidv 
 |-  ( f = F -> ( E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) <-> E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
33 23 32 raleqbidv 
 |-  ( f = F -> ( A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) <-> A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
34 33 ralbidv 
 |-  ( f = F -> ( A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) <-> A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
35 21 34 anbi12d 
 |-  ( f = F -> ( ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) <-> ( ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) )
36 35 opabbidv 
 |-  ( f = F -> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } )
37 oveq1 
 |-  ( w = W -> ( w J ( ( 1st ` F ) ` x ) ) = ( W J ( ( 1st ` F ) ` x ) ) )
38 37 eleq2d 
 |-  ( w = W -> ( m e. ( w J ( ( 1st ` F ) ` x ) ) <-> m e. ( W J ( ( 1st ` F ) ` x ) ) ) )
39 38 anbi2d 
 |-  ( w = W -> ( ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) <-> ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) ) )
40 oveq1 
 |-  ( w = W -> ( w J ( ( 1st ` F ) ` y ) ) = ( W J ( ( 1st ` F ) ` y ) ) )
41 opeq1 
 |-  ( w = W -> <. w , ( ( 1st ` F ) ` x ) >. = <. W , ( ( 1st ` F ) ` x ) >. )
42 41 oveq1d 
 |-  ( w = W -> ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) = ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) )
43 42 oveqd 
 |-  ( w = W -> ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) )
44 43 eqeq2d 
 |-  ( w = W -> ( g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) <-> g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
45 44 reubidv 
 |-  ( w = W -> ( E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) <-> E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
46 40 45 raleqbidv 
 |-  ( w = W -> ( A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) <-> A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
47 46 ralbidv 
 |-  ( w = W -> ( A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) <-> A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) )
48 39 47 anbi12d 
 |-  ( w = W -> ( ( ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) <-> ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) ) )
49 48 opabbidv 
 |-  ( w = W -> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. w , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } )
50 1 2 3 4 5 upfval 
 |-  ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } )
51 36 49 50 ovmpog 
 |-  ( ( F e. ( D Func E ) /\ W e. C /\ { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } e. _V ) -> ( F ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } )
52 7 6 16 51 syl3anc 
 |-  ( ph -> ( F ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( ( 1st ` F ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` F ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` F ) y ) ` k ) ( <. W , ( ( 1st ` F ) ` x ) >. O ( ( 1st ` F ) ` y ) ) m ) ) } )