Metamath Proof Explorer

Theorem diag1f1o

Description: The object part of the diagonal functor is a bijection if D is terminal. So any functor from a terminal category is one-to-one correspondent to an object of the target base. (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diag1f1o.a 
|- A = ( Base ` C )
diag1f1o.d 
|- ( ph -> D e. TermCat )
diag1f1o.c 
|- ( ph -> C e. Cat )
diag1f1o.l 
|- L = ( C DiagFunc D )
Assertion diag1f1o 
|- ( ph -> ( 1st ` L ) : A -1-1-onto-> ( D Func C ) )

Proof

Step Hyp Ref Expression
1 diag1f1o.a 
 |-  A = ( Base ` C )
2 diag1f1o.d 
 |-  ( ph -> D e. TermCat )
3 diag1f1o.c 
 |-  ( ph -> C e. Cat )
4 diag1f1o.l 
 |-  L = ( C DiagFunc D )
5 2 termccd 
 |-  ( ph -> D e. Cat )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 6 istermc2 
 |-  ( D e. TermCat <-> ( D e. ThinCat /\ E! y y e. ( Base ` D ) ) )
8 2 7 sylib 
 |-  ( ph -> ( D e. ThinCat /\ E! y y e. ( Base ` D ) ) )
9 8 simprd 
 |-  ( ph -> E! y y e. ( Base ` D ) )
10 euex 
 |-  ( E! y y e. ( Base ` D ) -> E. y y e. ( Base ` D ) )
11 9 10 syl 
 |-  ( ph -> E. y y e. ( Base ` D ) )
12 n0 
 |-  ( ( Base ` D ) =/= (/) <-> E. y y e. ( Base ` D ) )
13 11 12 sylibr 
 |-  ( ph -> ( Base ` D ) =/= (/) )
14 4 3 5 1 6 13 diag1f1 
 |-  ( ph -> ( 1st ` L ) : A -1-1-> ( D Func C ) )
15 f1f 
 |-  ( ( 1st ` L ) : A -1-1-> ( D Func C ) -> ( 1st ` L ) : A --> ( D Func C ) )
16 14 15 syl 
 |-  ( ph -> ( 1st ` L ) : A --> ( D Func C ) )
17 2 6 termcbas 
 |-  ( ph -> E. y ( Base ` D ) = { y } )
18 17 adantr 
 |-  ( ( ph /\ k e. ( D Func C ) ) -> E. y ( Base ` D ) = { y } )
19 fveq2 
 |-  ( x = ( ( 1st ` k ) ` y ) -> ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` ( ( 1st ` k ) ` y ) ) )
20 19 eqeq2d 
 |-  ( x = ( ( 1st ` k ) ` y ) -> ( k = ( ( 1st ` L ) ` x ) <-> k = ( ( 1st ` L ) ` ( ( 1st ` k ) ` y ) ) ) )
21 2 ad2antrr 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> D e. TermCat )
22 simplr 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> k e. ( D Func C ) )
23 vsnid 
 |-  y e. { y }
24 simpr 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> ( Base ` D ) = { y } )
25 23 24 eleqtrrid 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> y e. ( Base ` D ) )
26 eqid 
 |-  ( ( 1st ` k ) ` y ) = ( ( 1st ` k ) ` y )
27 1 21 22 6 25 26 4 diag1f1olem 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> ( ( ( 1st ` k ) ` y ) e. A /\ k = ( ( 1st ` L ) ` ( ( 1st ` k ) ` y ) ) ) )
28 27 simpld 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> ( ( 1st ` k ) ` y ) e. A )
29 27 simprd 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> k = ( ( 1st ` L ) ` ( ( 1st ` k ) ` y ) ) )
30 20 28 29 rspcedvdw 
 |-  ( ( ( ph /\ k e. ( D Func C ) ) /\ ( Base ` D ) = { y } ) -> E. x e. A k = ( ( 1st ` L ) ` x ) )
31 18 30 exlimddv 
 |-  ( ( ph /\ k e. ( D Func C ) ) -> E. x e. A k = ( ( 1st ` L ) ` x ) )
32 31 ralrimiva 
 |-  ( ph -> A. k e. ( D Func C ) E. x e. A k = ( ( 1st ` L ) ` x ) )
33 dffo3 
 |-  ( ( 1st ` L ) : A -onto-> ( D Func C ) <-> ( ( 1st ` L ) : A --> ( D Func C ) /\ A. k e. ( D Func C ) E. x e. A k = ( ( 1st ` L ) ` x ) ) )
34 16 32 33 sylanbrc 
 |-  ( ph -> ( 1st ` L ) : A -onto-> ( D Func C ) )
35 df-f1o 
 |-  ( ( 1st ` L ) : A -1-1-onto-> ( D Func C ) <-> ( ( 1st ` L ) : A -1-1-> ( D Func C ) /\ ( 1st ` L ) : A -onto-> ( D Func C ) ) )
36 14 34 35 sylanbrc 
 |-  ( ph -> ( 1st ` L ) : A -1-1-onto-> ( D Func C ) )