Metamath Proof Explorer

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 
|- ( A = (/) <-> TC+ A = (/) )

Proof

Step Hyp Ref Expression
1 ttceq 
 |-  ( A = (/) -> TC+ A = TC+ (/) )
2 ttc0 
 |-  TC+ (/) = (/)
3 1 2 eqtrdi 
 |-  ( A = (/) -> TC+ A = (/) )
4 ttcid 
 |-  A C_ TC+ A
5 sseq2 
 |-  ( TC+ A = (/) -> ( A C_ TC+ A <-> A C_ (/) ) )
6 4 5 mpbii 
 |-  ( TC+ A = (/) -> A C_ (/) )
7 ss0 
 |-  ( A C_ (/) -> A = (/) )
8 6 7 syl 
 |-  ( TC+ A = (/) -> A = (/) )
9 3 8 impbii 
 |-  ( A = (/) <-> TC+ A = (/) )