Metamath Proof Explorer

Theorem diag2f1

Description: If B is non-empty, the morphism part of a diagonal functor is injective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diag2f1.l 
|- L = ( C DiagFunc D )
diag2f1.a 
|- A = ( Base ` C )
diag2f1.b 
|- B = ( Base ` D )
diag2f1.h 
|- H = ( Hom ` C )
diag2f1.c 
|- ( ph -> C e. Cat )
diag2f1.d 
|- ( ph -> D e. Cat )
diag2f1.x 
|- ( ph -> X e. A )
diag2f1.y 
|- ( ph -> Y e. A )
diag2f1.0 
|- ( ph -> B =/= (/) )
diag2f1.n 
|- N = ( D Nat C )
Assertion diag2f1 
|- ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )

Proof

Step Hyp Ref Expression
1 diag2f1.l 
 |-  L = ( C DiagFunc D )
2 diag2f1.a 
 |-  A = ( Base ` C )
3 diag2f1.b 
 |-  B = ( Base ` D )
4 diag2f1.h 
 |-  H = ( Hom ` C )
5 diag2f1.c 
 |-  ( ph -> C e. Cat )
6 diag2f1.d 
 |-  ( ph -> D e. Cat )
7 diag2f1.x 
 |-  ( ph -> X e. A )
8 diag2f1.y 
 |-  ( ph -> Y e. A )
9 diag2f1.0 
 |-  ( ph -> B =/= (/) )
10 diag2f1.n 
 |-  N = ( D Nat C )
11 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
12 11 10 fuchom 
 |-  N = ( Hom ` ( D FuncCat C ) )
13 1 5 6 11 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
14 13 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
15 2 4 12 14 7 8 funcf2 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
16 5 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> C e. Cat )
17 6 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> D e. Cat )
18 7 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> X e. A )
19 8 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> Y e. A )
20 9 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> B =/= (/) )
21 simprl 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> f e. ( X H Y ) )
22 simprr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> g e. ( X H Y ) )
23 1 2 3 4 16 17 18 19 20 21 22 diag2f1lem 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> ( ( ( X ( 2nd ` L ) Y ) ` f ) = ( ( X ( 2nd ` L ) Y ) ` g ) -> f = g ) )
24 23 ralrimivva 
 |-  ( ph -> A. f e. ( X H Y ) A. g e. ( X H Y ) ( ( ( X ( 2nd ` L ) Y ) ` f ) = ( ( X ( 2nd ` L ) Y ) ` g ) -> f = g ) )
25 dff13 
 |-  ( ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) <-> ( ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) /\ A. f e. ( X H Y ) A. g e. ( X H Y ) ( ( ( X ( 2nd ` L ) Y ) ` f ) = ( ( X ( 2nd ` L ) Y ) ` g ) -> f = g ) ) )
26 15 24 25 sylanbrc 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )