Theorem ttcsntrsucg

Description: The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsntrsucg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Tr 𝐴 ) → TC+ { 𝐴 } = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ttcsng	⊢ ( 𝐴 ∈ 𝑉 → TC+ { 𝐴 } = ( TC+ 𝐴 ∪ { 𝐴 } ) )
2		ttctrid	⊢ ( Tr 𝐴 → TC+ 𝐴 = 𝐴 )
3	2	uneq1d	⊢ ( Tr 𝐴 → ( TC+ 𝐴 ∪ { 𝐴 } ) = ( 𝐴 ∪ { 𝐴 } ) )
4		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5	3 4	eqtr4di	⊢ ( Tr 𝐴 → ( TC+ 𝐴 ∪ { 𝐴 } ) = suc 𝐴 )
6	1 5	sylan9eq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Tr 𝐴 ) → TC+ { 𝐴 } = suc 𝐴 )