This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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