euendfunc

Description: If there exists a unique endofunctor (a functor from a category to itself) for a non-empty category, then the category is terminal. This partially explains why two categories are sufficient in termc2 . (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	euendfunc.f	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
	euendfunc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	euendfunc.0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
Assertion	euendfunc	⊢ ( 𝜑 → 𝐶 ∈ TermCat )

Proof

Step	Hyp	Ref	Expression
1		euendfunc.f	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
2		euendfunc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		euendfunc.0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
5	3 4	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐵 )
6		eqid	⊢ ( id_func ‘ 𝐶 ) = ( id_func ‘ 𝐶 )
7		eqid	⊢ ( 𝐶 Δ_func 𝐶 ) = ( 𝐶 Δ_func 𝐶 )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
9		euex	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
11		funcrcl	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) → ( 𝐶 ∈ Cat ∧ 𝐶 ∈ Cat ) )
12	11	simpld	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) → 𝐶 ∈ Cat )
13	12	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) → 𝐶 ∈ Cat )
14	10 13	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ Cat )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
16		eqid	⊢ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 )
17	6	idfucl	⊢ ( 𝐶 ∈ Cat → ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) )
18	14 17	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) )
19	7 14 14 2 15 16	diag1cl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) )
20		eumo	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) → ∃* 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
21	8 20	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
22		eleq1w	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ↔ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) )
23	22	mo4	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) → 𝑓 = 𝑔 ) )
24	21 23	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) → 𝑓 = 𝑔 ) )
25		fvex	⊢ ( id_func ‘ 𝐶 ) ∈ V
26		fvex	⊢ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ V
27		simpl	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → 𝑓 = ( id_func ‘ 𝐶 ) )
28	27	eleq1d	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ↔ ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ) )
29		simpr	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) )
30	29	eleq1d	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → ( 𝑔 ∈ ( 𝐶 Func 𝐶 ) ↔ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) )
31	28 30	anbi12d	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) ↔ ( ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) ) )
32		eqeq12	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → ( 𝑓 = 𝑔 ↔ ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) )
33	31 32	imbi12d	⊢ ( ( 𝑓 = ( id_func ‘ 𝐶 ) ∧ 𝑔 = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) → ( ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) → 𝑓 = 𝑔 ) ↔ ( ( ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) → ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) ) )
34	33	spc2gv	⊢ ( ( ( id_func ‘ 𝐶 ) ∈ V ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ V ) → ( ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) → 𝑓 = 𝑔 ) → ( ( ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) → ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) ) )
35	25 26 34	mp2an	⊢ ( ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝐶 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐶 ) ) → 𝑓 = 𝑔 ) → ( ( ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) → ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) )
36	24 35	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( id_func ‘ 𝐶 ) ∈ ( 𝐶 Func 𝐶 ) ∧ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐶 ) ) → ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) ) )
37	18 19 36	mp2and	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( id_func ‘ 𝐶 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐶 ) ) ‘ 𝑥 ) )
38	6 7 14 2 15 16 37	idfudiag1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ TermCat )
39	5 38	exlimddv	⊢ ( 𝜑 → 𝐶 ∈ TermCat )

Metamath Proof Explorer

Theorem euendfunc

Proof