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	⊢ ∅ ∈ Cat

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		base0	⊢ ∅ = ( Base ‘ ∅ )
3		0catg	⊢ ( ( ∅ ∈ V ∧ ∅ = ( Base ‘ ∅ ) ) → ∅ ∈ Cat )
4	1 2 3	mp2an	⊢ ∅ ∈ Cat