Metamath Proof Explorer

Theorem diag2f1o

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

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

Proof

Step Hyp Ref Expression
1 diag2f1o.l 
 |-  L = ( C DiagFunc D )
2 diag2f1o.a 
 |-  A = ( Base ` C )
3 diag2f1o.h 
 |-  H = ( Hom ` C )
4 diag2f1o.x 
 |-  ( ph -> X e. A )
5 diag2f1o.y 
 |-  ( ph -> Y e. A )
6 diag2f1o.n 
 |-  N = ( D Nat C )
7 diag2f1o.d 
 |-  ( ph -> D e. TermCat )
8 diag2f1o.c 
 |-  ( ph -> C e. Cat )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 7 termccd 
 |-  ( ph -> D e. Cat )
11 9 istermc2 
 |-  ( D e. TermCat <-> ( D e. ThinCat /\ E! z z e. ( Base ` D ) ) )
12 7 11 sylib 
 |-  ( ph -> ( D e. ThinCat /\ E! z z e. ( Base ` D ) ) )
13 12 simprd 
 |-  ( ph -> E! z z e. ( Base ` D ) )
14 euex 
 |-  ( E! z z e. ( Base ` D ) -> E. z z e. ( Base ` D ) )
15 13 14 syl 
 |-  ( ph -> E. z z e. ( Base ` D ) )
16 n0 
 |-  ( ( Base ` D ) =/= (/) <-> E. z z e. ( Base ` D ) )
17 15 16 sylibr 
 |-  ( ph -> ( Base ` D ) =/= (/) )
18 1 2 9 3 8 10 4 5 17 6 diag2f1 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
19 f1f 
 |-  ( ( 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 ) ) )
20 18 19 syl 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
21 7 9 termcbas 
 |-  ( ph -> E. z ( Base ` D ) = { z } )
22 21 adantr 
 |-  ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) -> E. z ( Base ` D ) = { z } )
23 fveq2 
 |-  ( f = ( m ` z ) -> ( ( X ( 2nd ` L ) Y ) ` f ) = ( ( X ( 2nd ` L ) Y ) ` ( m ` z ) ) )
24 23 eqeq2d 
 |-  ( f = ( m ` z ) -> ( m = ( ( X ( 2nd ` L ) Y ) ` f ) <-> m = ( ( X ( 2nd ` L ) Y ) ` ( m ` z ) ) ) )
25 4 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> X e. A )
26 5 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> Y e. A )
27 7 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> D e. TermCat )
28 simplr 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
29 vsnid 
 |-  z e. { z }
30 simpr 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> ( Base ` D ) = { z } )
31 29 30 eleqtrrid 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> z e. ( Base ` D ) )
32 eqid 
 |-  ( m ` z ) = ( m ` z )
33 1 2 3 25 26 6 27 28 9 31 32 diag2f1olem 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> ( ( m ` z ) e. ( X H Y ) /\ m = ( ( X ( 2nd ` L ) Y ) ` ( m ` z ) ) ) )
34 33 simpld 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> ( m ` z ) e. ( X H Y ) )
35 33 simprd 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> m = ( ( X ( 2nd ` L ) Y ) ` ( m ` z ) ) )
36 24 34 35 rspcedvdw 
 |-  ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> E. f e. ( X H Y ) m = ( ( X ( 2nd ` L ) Y ) ` f ) )
37 22 36 exlimddv 
 |-  ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) -> E. f e. ( X H Y ) m = ( ( X ( 2nd ` L ) Y ) ` f ) )
38 37 ralrimiva 
 |-  ( ph -> A. m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) E. f e. ( X H Y ) m = ( ( X ( 2nd ` L ) Y ) ` f ) )
39 dffo3 
 |-  ( ( X ( 2nd ` L ) Y ) : ( X H Y ) -onto-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) <-> ( ( X ( 2nd ` L ) Y ) : ( X H Y ) --> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) /\ A. m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) E. f e. ( X H Y ) m = ( ( X ( 2nd ` L ) Y ) ` f ) ) )
40 20 38 39 sylanbrc 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) -onto-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
41 df-f1o 
 |-  ( ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-onto-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) <-> ( ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) /\ ( X ( 2nd ` L ) Y ) : ( X H Y ) -onto-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) )
42 18 40 41 sylanbrc 
 |-  ( ph -> ( X ( 2nd ` L ) Y ) : ( X H Y ) -1-1-onto-> ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )