Metamath Proof Explorer

Theorem diag1

Description: The constant functor of X . (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses diag1.l 
|- L = ( C DiagFunc D )
diag1.c 
|- ( ph -> C e. Cat )
diag1.d 
|- ( ph -> D e. Cat )
diag1.a 
|- A = ( Base ` C )
diag1.x 
|- ( ph -> X e. A )
diag1.k 
|- K = ( ( 1st ` L ) ` X )
diag1.b 
|- B = ( Base ` D )
diag1.j 
|- J = ( Hom ` D )
diag1.i 
|- .1. = ( Id ` C )
Assertion diag1 
|- ( ph -> K = <. ( y e. B |-> X ) , ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) >. )

Proof

Step Hyp Ref Expression
1 diag1.l 
 |-  L = ( C DiagFunc D )
2 diag1.c 
 |-  ( ph -> C e. Cat )
3 diag1.d 
 |-  ( ph -> D e. Cat )
4 diag1.a 
 |-  A = ( Base ` C )
5 diag1.x 
 |-  ( ph -> X e. A )
6 diag1.k 
 |-  K = ( ( 1st ` L ) ` X )
7 diag1.b 
 |-  B = ( Base ` D )
8 diag1.j 
 |-  J = ( Hom ` D )
9 diag1.i 
 |-  .1. = ( Id ` C )
10 relfunc 
 |-  Rel ( D Func C )
11 1 2 3 4 5 6 diag1cl 
 |-  ( ph -> K e. ( D Func C ) )
12 1st2nd 
 |-  ( ( Rel ( D Func C ) /\ K e. ( D Func C ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
13 10 11 12 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
14 1st2ndbr 
 |-  ( ( Rel ( D Func C ) /\ K e. ( D Func C ) ) -> ( 1st ` K ) ( D Func C ) ( 2nd ` K ) )
15 10 11 14 sylancr 
 |-  ( ph -> ( 1st ` K ) ( D Func C ) ( 2nd ` K ) )
16 7 4 15 funcf1 
 |-  ( ph -> ( 1st ` K ) : B --> A )
17 16 feqmptd 
 |-  ( ph -> ( 1st ` K ) = ( y e. B |-> ( ( 1st ` K ) ` y ) ) )
18 2 adantr 
 |-  ( ( ph /\ y e. B ) -> C e. Cat )
19 3 adantr 
 |-  ( ( ph /\ y e. B ) -> D e. Cat )
20 5 adantr 
 |-  ( ( ph /\ y e. B ) -> X e. A )
21 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
22 1 18 19 4 20 6 7 21 diag11 
 |-  ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = X )
23 22 mpteq2dva 
 |-  ( ph -> ( y e. B |-> ( ( 1st ` K ) ` y ) ) = ( y e. B |-> X ) )
24 17 23 eqtrd 
 |-  ( ph -> ( 1st ` K ) = ( y e. B |-> X ) )
25 7 15 funcfn2 
 |-  ( ph -> ( 2nd ` K ) Fn ( B X. B ) )
26 fnov 
 |-  ( ( 2nd ` K ) Fn ( B X. B ) <-> ( 2nd ` K ) = ( y e. B , z e. B |-> ( y ( 2nd ` K ) z ) ) )
27 25 26 sylib 
 |-  ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( y ( 2nd ` K ) z ) ) )
28 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
29 15 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( 1st ` K ) ( D Func C ) ( 2nd ` K ) )
30 simp2 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> y e. B )
31 simp3 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> z e. B )
32 7 8 28 29 30 31 funcf2 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( y ( 2nd ` K ) z ) : ( y J z ) --> ( ( ( 1st ` K ) ` y ) ( Hom ` C ) ( ( 1st ` K ) ` z ) ) )
33 32 feqmptd 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( y ( 2nd ` K ) z ) = ( f e. ( y J z ) |-> ( ( y ( 2nd ` K ) z ) ` f ) ) )
34 simpl1 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> ph )
35 34 2 syl 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> C e. Cat )
36 34 3 syl 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> D e. Cat )
37 34 5 syl 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> X e. A )
38 30 adantr 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> y e. B )
39 31 adantr 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> z e. B )
40 simpr 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> f e. ( y J z ) )
41 1 35 36 4 37 6 7 38 8 9 39 40 diag12 
 |-  ( ( ( ph /\ y e. B /\ z e. B ) /\ f e. ( y J z ) ) -> ( ( y ( 2nd ` K ) z ) ` f ) = ( .1. ` X ) )
42 41 mpteq2dva 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( f e. ( y J z ) |-> ( ( y ( 2nd ` K ) z ) ` f ) ) = ( f e. ( y J z ) |-> ( .1. ` X ) ) )
43 33 42 eqtrd 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( y ( 2nd ` K ) z ) = ( f e. ( y J z ) |-> ( .1. ` X ) ) )
44 43 mpoeq3dva 
 |-  ( ph -> ( y e. B , z e. B |-> ( y ( 2nd ` K ) z ) ) = ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) )
45 27 44 eqtrd 
 |-  ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) )
46 24 45 opeq12d 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. = <. ( y e. B |-> X ) , ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) >. )
47 13 46 eqtrd 
 |-  ( ph -> K = <. ( y e. B |-> X ) , ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) >. )