Theorem idfudiag1bas

Description: If the identity functor of a category is the same as a constant functor to the category, then the base is a singleton. (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	idfudiag1bas	|- ( ph -> B = { X } )

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		eqid	|- ( Hom ` C ) = ( Hom ` C )
9	1 4 3 8	idfuval	|- ( ph -> I = <. ( _I |` B ) , ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) >. )
10		eqid	|- ( Id ` C ) = ( Id ` C )
11	2 3 3 4 5 6 4 8 10	diag1a	|- ( ph -> K = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` C ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. )
12	7 9 11	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 ) } ) ) >. )
13	4	fvexi	|- B e. _V
14		resiexg	|- ( B e. _V -> ( _I |` B ) e. _V )
15	13 14	ax-mp	|- ( _I |` B ) e. _V
16	13 13	xpex	|- ( B X. B ) e. _V
17	16	mptex	|- ( p e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` p ) ) ) e. _V
18	15 17	opth1	|- ( <. ( _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 } ) )
19	12 18	syl	|- ( ph -> ( _I |` B ) = ( B X. { X } ) )
20	5	ne0d	|- ( ph -> B =/= (/) )
21	19 20	idfudiag1lem	|- ( ph -> B = { X } )