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	|- ( ( A e. V /\ Tr A ) -> TC+ { A } = suc A )

Proof

Step	Hyp	Ref	Expression
1		ttcsng	|- ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) )
2		ttctrid	|- ( Tr A -> TC+ A = A )
3	2	uneq1d	|- ( Tr A -> ( TC+ A u. { A } ) = ( A u. { A } ) )
4		df-suc	|- suc A = ( A u. { A } )
5	3 4	eqtr4di	|- ( Tr A -> ( TC+ A u. { A } ) = suc A )
6	1 5	sylan9eq	|- ( ( A e. V /\ Tr A ) -> TC+ { A } = suc A )