Metamath Proof Explorer

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 
|- (/) e. Cat

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 base0 
 |-  (/) = ( Base ` (/) )
3 0catg 
 |-  ( ( (/) e. _V /\ (/) = ( Base ` (/) ) ) -> (/) e. Cat )
4 1 2 3 mp2an 
 |-  (/) e. Cat