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	Could not format assertion : No typesetting found for |- ( ( A e. V /\ Tr A ) -> TC+ { A } = suc A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcsng	Could not format ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) ) : No typesetting found for |- ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) ) with typecode |-
2		ttctrid	Could not format ( Tr A -> TC+ A = A ) : No typesetting found for |- ( Tr A -> TC+ A = A ) with typecode |-
3	2	uneq1d	Could not format ( Tr A -> ( TC+ A u. { A } ) = ( A u. { A } ) ) : No typesetting found for |- ( Tr A -> ( TC+ A u. { A } ) = ( A u. { A } ) ) with typecode |-
4		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
5	3 4	eqtr4di	Could not format ( Tr A -> ( TC+ A u. { A } ) = suc A ) : No typesetting found for |- ( Tr A -> ( TC+ A u. { A } ) = suc A ) with typecode |-
6	1 5	sylan9eq	Could not format ( ( A e. V /\ Tr A ) -> TC+ { A } = suc A ) : No typesetting found for |- ( ( A e. V /\ Tr A ) -> TC+ { A } = suc A ) with typecode |-