Theorem ttc0

Description: The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttc0	Could not format assertion : No typesetting found for |- TC+ (/) = (/) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		tr0	$$⊢\mathrm{Tr}\varnothing$$
2		ttctrid	Could not format ( Tr (/) -> TC+ (/) = (/) ) : No typesetting found for |- ( Tr (/) -> TC+ (/) = (/) ) with typecode |-
3	1 2	ax-mp	Could not format TC+ (/) = (/) : No typesetting found for |- TC+ (/) = (/) with typecode |-