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	⊢ TC+ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		tr0	⊢ Tr ∅
2		ttctrid	⊢ ( Tr ∅ → TC+ ∅ = ∅ )
3	1 2	ax-mp	⊢ TC+ ∅ = ∅