Metamath Proof Explorer

Theorem diag1a

Description: The constant functor of X . (Contributed by Zhi Wang, 19-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 diag1a 
|- ( ph -> K = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y J z ) X. { ( .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 1 2 3 4 5 6 7 8 9 diag1 
 |-  ( ph -> K = <. ( y e. B |-> X ) , ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) >. )
11 fconstmpt 
 |-  ( B X. { X } ) = ( y e. B |-> X )
12 fconstmpt 
 |-  ( ( y J z ) X. { ( .1. ` X ) } ) = ( f e. ( y J z ) |-> ( .1. ` X ) )
13 12 a1i 
 |-  ( ( y e. B /\ z e. B ) -> ( ( y J z ) X. { ( .1. ` X ) } ) = ( f e. ( y J z ) |-> ( .1. ` X ) ) )
14 13 mpoeq3ia 
 |-  ( y e. B , z e. B |-> ( ( y J z ) X. { ( .1. ` X ) } ) ) = ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) )
15 11 14 opeq12i 
 |-  <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y J z ) X. { ( .1. ` X ) } ) ) >. = <. ( y e. B |-> X ) , ( y e. B , z e. B |-> ( f e. ( y J z ) |-> ( .1. ` X ) ) ) >.
16 10 15 eqtr4di 
 |-  ( ph -> K = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y J z ) X. { ( .1. ` X ) } ) ) >. )