Metamath Proof Explorer

Theorem prcofdiag1

Description: A constant functor pre-composed by a functor is another constant functor. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses prcofdiag.l 
|- L = ( C DiagFunc D )
prcofdiag.m 
|- M = ( C DiagFunc E )
prcofdiag.f 
|- ( ph -> F e. ( E Func D ) )
prcofdiag.c 
|- ( ph -> C e. Cat )
prcofdiag1.b 
|- B = ( Base ` C )
prcofdiag1.x 
|- ( ph -> X e. B )
Assertion prcofdiag1 
|- ( ph -> ( ( ( 1st ` L ) ` X ) o.func F ) = ( ( 1st ` M ) ` X ) )

Proof

Step Hyp Ref Expression
1 prcofdiag.l 
 |-  L = ( C DiagFunc D )
2 prcofdiag.m 
 |-  M = ( C DiagFunc E )
3 prcofdiag.f 
 |-  ( ph -> F e. ( E Func D ) )
4 prcofdiag.c 
 |-  ( ph -> C e. Cat )
5 prcofdiag1.b 
 |-  B = ( Base ` C )
6 prcofdiag1.x 
 |-  ( ph -> X e. B )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 3 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( E Func D ) ( 2nd ` F ) )
9 8 funcrcl3 
 |-  ( ph -> D e. Cat )
10 eqid 
 |-  ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
11 1 4 9 5 6 10 diag1cl 
 |-  ( ph -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
12 3 11 cofucl 
 |-  ( ph -> ( ( ( 1st ` L ) ` X ) o.func F ) e. ( E Func C ) )
13 12 func1st2nd 
 |-  ( ph -> ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ( E Func C ) ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) )
14 7 5 13 funcf1 
 |-  ( ph -> ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) : ( Base ` E ) --> B )
15 14 ffnd 
 |-  ( ph -> ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) Fn ( Base ` E ) )
16 8 funcrcl2 
 |-  ( ph -> E e. Cat )
17 eqid 
 |-  ( ( 1st ` M ) ` X ) = ( ( 1st ` M ) ` X )
18 2 4 16 5 6 17 diag1cl 
 |-  ( ph -> ( ( 1st ` M ) ` X ) e. ( E Func C ) )
19 18 func1st2nd 
 |-  ( ph -> ( 1st ` ( ( 1st ` M ) ` X ) ) ( E Func C ) ( 2nd ` ( ( 1st ` M ) ` X ) ) )
20 7 5 19 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` M ) ` X ) ) : ( Base ` E ) --> B )
21 20 ffnd 
 |-  ( ph -> ( 1st ` ( ( 1st ` M ) ` X ) ) Fn ( Base ` E ) )
22 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> C e. Cat )
23 9 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> D e. Cat )
24 6 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> X e. B )
25 eqid 
 |-  ( Base ` D ) = ( Base ` D )
26 7 25 8 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` E ) --> ( Base ` D ) )
27 26 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
28 1 22 23 5 24 10 25 27 diag11 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` ( ( 1st ` F ) ` x ) ) = X )
29 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> F e. ( E Func D ) )
30 11 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
31 simpr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> x e. ( Base ` E ) )
32 7 29 30 31 cofu1 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ` x ) = ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` ( ( 1st ` F ) ` x ) ) )
33 16 adantr 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> E e. Cat )
34 2 22 33 5 24 17 7 31 diag11 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` ( ( 1st ` M ) ` X ) ) ` x ) = X )
35 28 32 34 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> ( ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ` x ) = ( ( 1st ` ( ( 1st ` M ) ` X ) ) ` x ) )
36 15 21 35 eqfnfvd 
 |-  ( ph -> ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) = ( 1st ` ( ( 1st ` M ) ` X ) ) )
37 7 13 funcfn2 
 |-  ( ph -> ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) Fn ( ( Base ` E ) X. ( Base ` E ) ) )
38 7 19 funcfn2 
 |-  ( ph -> ( 2nd ` ( ( 1st ` M ) ` X ) ) Fn ( ( Base ` E ) X. ( Base ` E ) ) )
39 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
40 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
41 13 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ( E Func C ) ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) )
42 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> x e. ( Base ` E ) )
43 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> y e. ( Base ` E ) )
44 7 39 40 41 42 43 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( x ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) y ) : ( x ( Hom ` E ) y ) --> ( ( ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ` x ) ( Hom ` C ) ( ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) ` y ) ) )
45 44 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( x ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) y ) Fn ( x ( Hom ` E ) y ) )
46 19 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( 1st ` ( ( 1st ` M ) ` X ) ) ( E Func C ) ( 2nd ` ( ( 1st ` M ) ` X ) ) )
47 7 39 40 46 42 43 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( x ( 2nd ` ( ( 1st ` M ) ` X ) ) y ) : ( x ( Hom ` E ) y ) --> ( ( ( 1st ` ( ( 1st ` M ) ` X ) ) ` x ) ( Hom ` C ) ( ( 1st ` ( ( 1st ` M ) ` X ) ) ` y ) ) )
48 47 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( x ( 2nd ` ( ( 1st ` M ) ` X ) ) y ) Fn ( x ( Hom ` E ) y ) )
49 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> C e. Cat )
50 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> D e. Cat )
51 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> X e. B )
52 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( 1st ` F ) ( E Func D ) ( 2nd ` F ) )
53 7 25 52 funcf1 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( 1st ` F ) : ( Base ` E ) --> ( Base ` D ) )
54 42 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> x e. ( Base ` E ) )
55 53 54 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
56 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
57 eqid 
 |-  ( Id ` C ) = ( Id ` C )
58 43 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> y e. ( Base ` E ) )
59 53 58 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
60 7 39 56 52 54 58 funcf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` E ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
61 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> f e. ( x ( Hom ` E ) y ) )
62 60 61 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
63 1 49 50 5 51 10 25 55 56 57 59 62 diag12 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( ( 1st ` L ) ` X ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( Id ` C ) ` X ) )
64 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> F e. ( E Func D ) )
65 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( 1st ` L ) ` X ) e. ( D Func C ) )
66 7 64 65 54 58 39 61 cofu2 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( x ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) y ) ` f ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( ( 1st ` L ) ` X ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
67 16 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> E e. Cat )
68 2 49 67 5 51 17 7 54 39 57 58 61 diag12 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( x ( 2nd ` ( ( 1st ` M ) ` X ) ) y ) ` f ) = ( ( Id ` C ) ` X ) )
69 63 66 68 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) /\ f e. ( x ( Hom ` E ) y ) ) -> ( ( x ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) y ) ` f ) = ( ( x ( 2nd ` ( ( 1st ` M ) ` X ) ) y ) ` f ) )
70 45 48 69 eqfnfvd 
 |-  ( ( ph /\ ( x e. ( Base ` E ) /\ y e. ( Base ` E ) ) ) -> ( x ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) y ) = ( x ( 2nd ` ( ( 1st ` M ) ` X ) ) y ) )
71 37 38 70 eqfnovd 
 |-  ( ph -> ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) = ( 2nd ` ( ( 1st ` M ) ` X ) ) )
72 36 71 opeq12d 
 |-  ( ph -> <. ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) , ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) >. = <. ( 1st ` ( ( 1st ` M ) ` X ) ) , ( 2nd ` ( ( 1st ` M ) ` X ) ) >. )
73 relfunc 
 |-  Rel ( E Func C )
74 1st2nd 
 |-  ( ( Rel ( E Func C ) /\ ( ( ( 1st ` L ) ` X ) o.func F ) e. ( E Func C ) ) -> ( ( ( 1st ` L ) ` X ) o.func F ) = <. ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) , ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) >. )
75 73 12 74 sylancr 
 |-  ( ph -> ( ( ( 1st ` L ) ` X ) o.func F ) = <. ( 1st ` ( ( ( 1st ` L ) ` X ) o.func F ) ) , ( 2nd ` ( ( ( 1st ` L ) ` X ) o.func F ) ) >. )
76 1st2nd 
 |-  ( ( Rel ( E Func C ) /\ ( ( 1st ` M ) ` X ) e. ( E Func C ) ) -> ( ( 1st ` M ) ` X ) = <. ( 1st ` ( ( 1st ` M ) ` X ) ) , ( 2nd ` ( ( 1st ` M ) ` X ) ) >. )
77 73 18 76 sylancr 
 |-  ( ph -> ( ( 1st ` M ) ` X ) = <. ( 1st ` ( ( 1st ` M ) ` X ) ) , ( 2nd ` ( ( 1st ` M ) ` X ) ) >. )
78 72 75 77 3eqtr4d 
 |-  ( ph -> ( ( ( 1st ` L ) ` X ) o.func F ) = ( ( 1st ` M ) ` X ) )