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

Metamath Proof Explorer

Theorem idfudiag1

Description: If the identity functor of a category is the same as a constant functor to the category, then the category is terminal. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypotheses idfudiag1.i 
|- I = ( idFunc ` C )
idfudiag1.l 
|- L = ( C DiagFunc C )
idfudiag1.c 
|- ( ph -> C e. Cat )
idfudiag1.b 
|- B = ( Base ` C )
idfudiag1.x 
|- ( ph -> X e. B )
idfudiag1.k 
|- K = ( ( 1st ` L ) ` X )
idfudiag1.e 
|- ( ph -> I = K )
Assertion idfudiag1 
|- ( ph -> C e. TermCat )

Proof

Step Hyp Ref Expression
1 idfudiag1.i 
 |-  I = ( idFunc ` C )
2 idfudiag1.l 
 |-  L = ( C DiagFunc C )
3 idfudiag1.c 
 |-  ( ph -> C e. Cat )
4 idfudiag1.b 
 |-  B = ( Base ` C )
5 idfudiag1.x 
 |-  ( ph -> X e. B )
6 idfudiag1.k 
 |-  K = ( ( 1st ` L ) ` X )
7 idfudiag1.e 
 |-  ( ph -> I = K )
8 4 a1i 
 |-  ( ph -> B = ( Base ` C ) )
9 eqidd 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` C ) )
10 fveq2 
 |-  ( p = <. y , z >. -> ( ( Hom ` C ) ` p ) = ( ( Hom ` C ) ` <. y , z >. ) )
11 df-ov 
 |-  ( y ( Hom ` C ) z ) = ( ( Hom ` C ) ` <. y , z >. )
12 10 11 eqtr4di 
 |-  ( p = <. y , z >. -> ( ( Hom ` C ) ` p ) = ( y ( Hom ` C ) z ) )
13 12 reseq2d 
 |-  ( p = <. y , z >. -> ( _I |` ( ( Hom ` C ) ` p ) ) = ( _I |` ( y ( Hom ` C ) z ) ) )
14 13 mpompt 
 |-  ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) = ( y e. B , z e. B |-> ( _I |` ( y ( Hom ` C ) z ) ) )
15 14 a1i 
 |-  ( ph -> ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) = ( y e. B , z e. B |-> ( _I |` ( y ( Hom ` C ) z ) ) ) )
16 ovex 
 |-  ( y ( Hom ` C ) z ) e. _V
17 resiexg 
 |-  ( ( y ( Hom ` C ) z ) e. _V -> ( _I |` ( y ( Hom ` C ) z ) ) e. _V )
18 16 17 mp1i 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( _I |` ( y ( Hom ` C ) z ) ) e. _V )
19 15 18 ovmpt4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) z ) = ( _I |` ( y ( Hom ` C ) z ) ) )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 1 4 3 20 idfuval 
 |-  ( ph -> I = <. ( _I |` B ) , ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) >. )
22 eqid 
 |-  ( Id ` C ) = ( Id ` C )
23 2 3 3 4 5 6 4 20 22 diag1a 
 |-  ( ph -> K = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. )
24 7 21 23 3eqtr3d 
 |-  ( ph -> <. ( _I |` B ) , ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) >. = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. )
25 4 fvexi 
 |-  B e. _V
26 resiexg 
 |-  ( B e. _V -> ( _I |` B ) e. _V )
27 25 26 ax-mp 
 |-  ( _I |` B ) e. _V
28 25 25 xpex 
 |-  ( B X. B ) e. _V
29 28 mptex 
 |-  ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) e. _V
30 27 29 opth 
 |-  ( <. ( _I |` B ) , ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) >. = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. <-> ( ( _I |` B ) = ( B X. { X } ) /\ ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) = ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) ) )
31 30 simprbi 
 |-  ( <. ( _I |` B ) , ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) >. = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. -> ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) = ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) )
32 24 31 syl 
 |-  ( ph -> ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) = ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) )
33 snex 
 |-  { ( ( Id ` C ) ` X ) } e. _V
34 16 33 xpex 
 |-  ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) e. _V
35 34 a1i 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) e. _V )
36 32 35 ovmpt4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) z ) = ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) )
37 19 36 eqtr3d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( _I |` ( y ( Hom ` C ) z ) ) = ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) )
38 3 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> C e. Cat )
39 simprl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. B )
40 4 20 22 38 39 catidcl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( Id ` C ) ` y ) e. ( y ( Hom ` C ) y ) )
41 1 2 3 4 5 6 7 idfudiag1bas 
 |-  ( ph -> B = { X } )
42 41 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> B = { X } )
43 39 42 eleqtrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. { X } )
44 elsni 
 |-  ( y e. { X } -> y = X )
45 43 44 syl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y = X )
46 simprr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. B )
47 46 42 eleqtrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. { X } )
48 elsni 
 |-  ( z e. { X } -> z = X )
49 47 48 syl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z = X )
50 45 49 eqtr4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y = z )
51 50 oveq2d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( Hom ` C ) y ) = ( y ( Hom ` C ) z ) )
52 40 51 eleqtrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( Id ` C ) ` y ) e. ( y ( Hom ` C ) z ) )
53 52 ne0d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( Hom ` C ) z ) =/= (/) )
54 37 53 idfudiag1lem 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( Hom ` C ) z ) = { ( ( Id ` C ) ` X ) } )
55 mosn 
 |-  ( ( y ( Hom ` C ) z ) = { ( ( Id ` C ) ` X ) } -> E* f f e. ( y ( Hom ` C ) z ) )
56 54 55 syl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> E* f f e. ( y ( Hom ` C ) z ) )
57 8 9 56 3 isthincd 
 |-  ( ph -> C e. ThinCat )
58 sneq 
 |-  ( x = X -> { x } = { X } )
59 58 eqeq2d 
 |-  ( x = X -> ( B = { x } <-> B = { X } ) )
60 5 41 59 spcedv 
 |-  ( ph -> E. x B = { x } )
61 4 istermc 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) )
62 57 60 61 sylanbrc 
 |-  ( ph -> C e. TermCat )