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 } )

Metamath Proof Explorer

Theorem idfudiag1bas

Proof