Theorem ttc00

Description: A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttc00	⊢ ( 𝐴 = ∅ ↔ TC+ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ttceq	⊢ ( 𝐴 = ∅ → TC+ 𝐴 = TC+ ∅ )
2		ttc0	⊢ TC+ ∅ = ∅
3	1 2	eqtrdi	⊢ ( 𝐴 = ∅ → TC+ 𝐴 = ∅ )
4		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
5		sseq2	⊢ ( TC+ 𝐴 = ∅ → ( 𝐴 ⊆ TC+ 𝐴 ↔ 𝐴 ⊆ ∅ ) )
6	4 5	mpbii	⊢ ( TC+ 𝐴 = ∅ → 𝐴 ⊆ ∅ )
7		ss0	⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
8	6 7	syl	⊢ ( TC+ 𝐴 = ∅ → 𝐴 = ∅ )
9	3 8	impbii	⊢ ( 𝐴 = ∅ ↔ TC+ 𝐴 = ∅ )