Metamath Proof Explorer

Theorem 0thinc

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

Ref Expression
Assertion 0thinc 
|- (/) e. ThinCat

Proof

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