Theorem ttctrid

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

	Ref	Expression
Assertion	ttctrid	⊢ ( Tr 𝐴 → TC+ 𝐴 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		ttcmin	⊢ ( ( 𝐴 ⊆ 𝐴 ∧ Tr 𝐴 ) → TC+ 𝐴 ⊆ 𝐴 )
3	1 2	mpan	⊢ ( Tr 𝐴 → TC+ 𝐴 ⊆ 𝐴 )
4		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
5	4	a1i	⊢ ( Tr 𝐴 → 𝐴 ⊆ TC+ 𝐴 )
6	3 5	eqssd	⊢ ( Tr 𝐴 → TC+ 𝐴 = 𝐴 )