Theorem 0thinc

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

	Ref	Expression
Assertion	0thinc	Could not format assertion : No typesetting found for |- (/) e. ThinCat with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
3		0thincg	Could not format ( ( (/) e. _V /\ (/) = ( Base ` (/) ) ) -> (/) e. ThinCat ) : No typesetting found for |- ( ( (/) e. _V /\ (/) = ( Base ` (/) ) ) -> (/) e. ThinCat ) with typecode |-
4	1 2 3	mp2an	Could not format (/) e. ThinCat : No typesetting found for |- (/) e. ThinCat with typecode |-