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

Metamath Proof Explorer

Theorem 0thinc

Description: The empty category (see 0cat ) is thin. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion 0thinc ⊢ ∅ ∈ ThinCat

Proof

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