This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem diag2cl

Description: The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses diag2.l 
|- L = ( C DiagFunc D )
diag2.a 
|- A = ( Base ` C )
diag2.b 
|- B = ( Base ` D )
diag2.h 
|- H = ( Hom ` C )
diag2.c 
|- ( ph -> C e. Cat )
diag2.d 
|- ( ph -> D e. Cat )
diag2.x 
|- ( ph -> X e. A )
diag2.y 
|- ( ph -> Y e. A )
diag2.f 
|- ( ph -> F e. ( X H Y ) )
diag2cl.h 
|- N = ( D Nat C )
Assertion diag2cl 
|- ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )

Proof

Step Hyp Ref Expression
1 diag2.l 
 |-  L = ( C DiagFunc D )
2 diag2.a 
 |-  A = ( Base ` C )
3 diag2.b 
 |-  B = ( Base ` D )
4 diag2.h 
 |-  H = ( Hom ` C )
5 diag2.c 
 |-  ( ph -> C e. Cat )
6 diag2.d 
 |-  ( ph -> D e. Cat )
7 diag2.x 
 |-  ( ph -> X e. A )
8 diag2.y 
 |-  ( ph -> Y e. A )
9 diag2.f 
 |-  ( ph -> F e. ( X H Y ) )
10 diag2cl.h 
 |-  N = ( D Nat C )
11 1 2 3 4 5 6 7 8 9 diag2 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
12 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
13 12 10 fuchom 
 |-  N = ( Hom ` ( D FuncCat C ) )
14 relfunc 
 |-  Rel ( C Func ( D FuncCat C ) )
15 1 5 6 12 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
16 1st2ndbr 
 |-  ( ( Rel ( C Func ( D FuncCat C ) ) /\ L e. ( C Func ( D FuncCat C ) ) ) -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
17 14 15 16 sylancr 
 |-  ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
18 2 4 13 17 7 8 funcf2 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
19 18 9 ffvelcdmd 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
20 11 19 eqeltrrd 
 |-  ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )