Theorem 0cat

Description: The empty set is a category, theempty category, see example 3.3(4.c) in Adamek p. 24. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Assertion	0cat	$$⊢\varnothing \in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
3		0catg	$$⊢\left(\varnothing \in \mathrm{V}\wedge \varnothing ={\mathrm{Base}}_{\varnothing }\right)\to \varnothing \in \mathrm{Cat}$$
4	1 2 3	mp2an	$$⊢\varnothing \in \mathrm{Cat}$$