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	⊢ 𝐼 = ( id_func ‘ 𝐶 )
	idfudiag1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐶 )
	idfudiag1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	idfudiag1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	idfudiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	idfudiag1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	idfudiag1.e	⊢ ( 𝜑 → 𝐼 = 𝐾 )
Assertion	idfudiag1bas	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		idfudiag1.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
2		idfudiag1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐶 )
3		idfudiag1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		idfudiag1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5		idfudiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		idfudiag1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
7		idfudiag1.e	⊢ ( 𝜑 → 𝐼 = 𝐾 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9	1 4 3 8	idfuval	⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ )
10		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11	2 3 3 4 5 6 4 8 10	diag1a	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
12	7 9 11	3eqtr3d	⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
13	4	fvexi	⊢ 𝐵 ∈ V
14		resiexg	⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
15	13 14	ax-mp	⊢ ( I ↾ 𝐵 ) ∈ V
16	13 13	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
17	16	mptex	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ∈ V
18	15 17	opth1	⊢ ( ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ → ( I ↾ 𝐵 ) = ( 𝐵 × { 𝑋 } ) )
19	12 18	syl	⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( 𝐵 × { 𝑋 } ) )
20	5	ne0d	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
21	19 20	idfudiag1lem	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )

Metamath Proof Explorer

Theorem idfudiag1bas

Proof