initc

Description: Sets with empty base are the only initial objects in the category of small categories. Example 7.2(3) of Adamek p. 101. (Contributed by Zhi Wang, 15-Nov-2025)

		Ref	Expression
	Assertion	initc	$⊢ (C \in V \land \emptyset = {Base}_{C}) \leftrightarrow \forall d \in Cat \exists! f f \in (C Func d)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to C \in V$
2		simplr	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to \emptyset = {Base}_{C}$
3		simpr	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to d \in Cat$
4	1 2 3	0funcg	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to C Func d = \{⟨\emptyset, \emptyset⟩\}$
5		opex	$⊢ ⟨\emptyset, \emptyset⟩ \in V$
6		sneq	$⊢ f = ⟨\emptyset, \emptyset⟩ \to \{f\} = \{⟨\emptyset, \emptyset⟩\}$
7	6	eqeq2d	$⊢ f = ⟨\emptyset, \emptyset⟩ \to (C Func d = \{f\} \leftrightarrow C Func d = \{⟨\emptyset, \emptyset⟩\})$
8	5 7	spcev	$⊢ C Func d = \{⟨\emptyset, \emptyset⟩\} \to \exists f C Func d = \{f\}$
9	4 8	syl	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to \exists f C Func d = \{f\}$
10		eusn	$⊢ \exists! f f \in (C Func d) \leftrightarrow \exists f C Func d = \{f\}$
11	9 10	sylibr	$⊢ ((C \in V \land \emptyset = {Base}_{C}) \land d \in Cat) \to \exists! f f \in (C Func d)$
12	11	ralrimiva	$⊢ (C \in V \land \emptyset = {Base}_{C}) \to \forall d \in Cat \exists! f f \in (C Func d)$
13		0cat	$⊢ \emptyset \in Cat$
14		oveq2	$⊢ d = \emptyset \to C Func d = C Func \emptyset$
15	14	eleq2d	$⊢ d = \emptyset \to (f \in (C Func d) \leftrightarrow f \in (C Func \emptyset))$
16	15	eubidv	$⊢ d = \emptyset \to (\exists! f f \in (C Func d) \leftrightarrow \exists! f f \in (C Func \emptyset))$
17	16	rspcv	$⊢ \emptyset \in Cat \to (\forall d \in Cat \exists! f f \in (C Func d) \to \exists! f f \in (C Func \emptyset))$
18	13 17	ax-mp	$⊢ \forall d \in Cat \exists! f f \in (C Func d) \to \exists! f f \in (C Func \emptyset)$
19		euex	$⊢ \exists! f f \in (C Func \emptyset) \to \exists f f \in (C Func \emptyset)$
20		funcrcl	$⊢ f \in (C Func \emptyset) \to (C \in Cat \land \emptyset \in Cat)$
21	20	simpld	$⊢ f \in (C Func \emptyset) \to C \in Cat$
22	21	elexd	$⊢ f \in (C Func \emptyset) \to C \in V$
23		eqid	$⊢ {Base}_{C} = {Base}_{C}$
24		base0	$⊢ \emptyset = {Base}_{\emptyset}$
25		eqidd	$⊢ f \in (C Func \emptyset) \to \emptyset = \emptyset$
26		id	$⊢ f \in (C Func \emptyset) \to f \in (C Func \emptyset)$
27	23 24 25 26	func0g2	$⊢ f \in (C Func \emptyset) \to {Base}_{C} = \emptyset$
28	27	eqcomd	$⊢ f \in (C Func \emptyset) \to \emptyset = {Base}_{C}$
29	22 28	jca	$⊢ f \in (C Func \emptyset) \to (C \in V \land \emptyset = {Base}_{C})$
30	29	exlimiv	$⊢ \exists f f \in (C Func \emptyset) \to (C \in V \land \emptyset = {Base}_{C})$
31	18 19 30	3syl	$⊢ \forall d \in Cat \exists! f f \in (C Func d) \to (C \in V \land \emptyset = {Base}_{C})$
32	12 31	impbii	$⊢ (C \in V \land \emptyset = {Base}_{C}) \leftrightarrow \forall d \in Cat \exists! f f \in (C Func d)$

Metamath Proof Explorer

Theorem initc

Proof