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	$⊢ φ \to \exists! f f \in (C Func C)$
	euendfunc.b	$⊢ B = {Base}_{C}$
	euendfunc.0	$⊢ φ \to B \neq \emptyset$
Assertion	euendfunc	Could not format assertion : No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		euendfunc.f	$⊢ φ \to \exists! f f \in (C Func C)$
2		euendfunc.b	$⊢ B = {Base}_{C}$
3		euendfunc.0	$⊢ φ \to B \neq \emptyset$
4		n0	$⊢ B \neq \emptyset \leftrightarrow \exists x x \in B$
5	3 4	sylib	$⊢ φ \to \exists x x \in B$
6		eqid	$⊢ {id}_{func} (C) = {id}_{func} (C)$
7		eqid	$⊢ C Δ_{func} C = C Δ_{func} C$
8	1	adantr	$⊢ (φ \land x \in B) \to \exists! f f \in (C Func C)$
9		euex	$⊢ \exists! f f \in (C Func C) \to \exists f f \in (C Func C)$
10	8 9	syl	$⊢ (φ \land x \in B) \to \exists f f \in (C Func C)$
11		funcrcl	$⊢ f \in (C Func C) \to (C \in Cat \land C \in Cat)$
12	11	simpld	$⊢ f \in (C Func C) \to C \in Cat$
13	12	exlimiv	$⊢ \exists f f \in (C Func C) \to C \in Cat$
14	10 13	syl	$⊢ (φ \land x \in B) \to C \in Cat$
15		simpr	$⊢ (φ \land x \in B) \to x \in B$
16		eqid	$⊢ 1^{st} (C Δ_{func} C) (x) = 1^{st} (C Δ_{func} C) (x)$
17	6	idfucl	$⊢ C \in Cat \to {id}_{func} (C) \in (C Func C)$
18	14 17	syl	$⊢ (φ \land x \in B) \to {id}_{func} (C) \in (C Func C)$
19	7 14 14 2 15 16	diag1cl	$⊢ (φ \land x \in B) \to 1^{st} (C Δ_{func} C) (x) \in (C Func C)$
20		eumo	$⊢ \exists! f f \in (C Func C) \to \exists^{*} f f \in (C Func C)$
21	8 20	syl	$⊢ (φ \land x \in B) \to \exists^{*} f f \in (C Func C)$
22		eleq1w	$⊢ f = g \to (f \in (C Func C) \leftrightarrow g \in (C Func C))$
23	22	mo4	$⊢ \exists^{*} f f \in (C Func C) \leftrightarrow \forall f \forall g ((f \in (C Func C) \land g \in (C Func C)) \to f = g)$
24	21 23	sylib	$⊢ (φ \land x \in B) \to \forall f \forall g ((f \in (C Func C) \land g \in (C Func C)) \to f = g)$
25		fvex	$⊢ {id}_{func} (C) \in V$
26		fvex	$⊢ 1^{st} (C Δ_{func} C) (x) \in V$
27		simpl	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to f = {id}_{func} (C)$
28	27	eleq1d	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to (f \in (C Func C) \leftrightarrow {id}_{func} (C) \in (C Func C))$
29		simpr	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to g = 1^{st} (C Δ_{func} C) (x)$
30	29	eleq1d	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to (g \in (C Func C) \leftrightarrow 1^{st} (C Δ_{func} C) (x) \in (C Func C))$
31	28 30	anbi12d	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to ((f \in (C Func C) \land g \in (C Func C)) \leftrightarrow ({id}_{func} (C) \in (C Func C) \land 1^{st} (C Δ_{func} C) (x) \in (C Func C)))$
32		eqeq12	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to (f = g \leftrightarrow {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x))$
33	31 32	imbi12d	$⊢ (f = {id}_{func} (C) \land g = 1^{st} (C Δ_{func} C) (x)) \to (((f \in (C Func C) \land g \in (C Func C)) \to f = g) \leftrightarrow (({id}_{func} (C) \in (C Func C) \land 1^{st} (C Δ_{func} C) (x) \in (C Func C)) \to {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x)))$
34	33	spc2gv	$⊢ ({id}_{func} (C) \in V \land 1^{st} (C Δ_{func} C) (x) \in V) \to (\forall f \forall g ((f \in (C Func C) \land g \in (C Func C)) \to f = g) \to (({id}_{func} (C) \in (C Func C) \land 1^{st} (C Δ_{func} C) (x) \in (C Func C)) \to {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x)))$
35	25 26 34	mp2an	$⊢ \forall f \forall g ((f \in (C Func C) \land g \in (C Func C)) \to f = g) \to (({id}_{func} (C) \in (C Func C) \land 1^{st} (C Δ_{func} C) (x) \in (C Func C)) \to {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x))$
36	24 35	syl	$⊢ (φ \land x \in B) \to (({id}_{func} (C) \in (C Func C) \land 1^{st} (C Δ_{func} C) (x) \in (C Func C)) \to {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x))$
37	18 19 36	mp2and	$⊢ (φ \land x \in B) \to {id}_{func} (C) = 1^{st} (C Δ_{func} C) (x)$
38	6 7 14 2 15 16 37	idfudiag1	Could not format ( ( ph /\ x e. B ) -> C e. TermCat ) : No typesetting found for \|- ( ( ph /\ x e. B ) -> C e. TermCat ) with typecode \|-
39	5 38	exlimddv	Could not format ( ph -> C e. TermCat ) : No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-

Metamath Proof Explorer

Theorem euendfunc

Proof