Theorem ttcexg

Description: The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcexg	|- ( A e. V -> TC+ A e. _V )

Proof

Step	Hyp	Ref	Expression
1		sseq1	|- ( x = A -> ( x C_ y <-> A C_ y ) )
2	1	anbi1d	|- ( x = A -> ( ( x C_ y /\ Tr y ) <-> ( A C_ y /\ Tr y ) ) )
3	2	exbidv	|- ( x = A -> ( E. y ( x C_ y /\ Tr y ) <-> E. y ( A C_ y /\ Tr y ) ) )
4		vex	|- x e. _V
5	4	tz9.1	|- E. y ( x C_ y /\ Tr y /\ A. z ( ( x C_ z /\ Tr z ) -> y C_ z ) )
6		3simpa	|- ( ( x C_ y /\ Tr y /\ A. z ( ( x C_ z /\ Tr z ) -> y C_ z ) ) -> ( x C_ y /\ Tr y ) )
7	5 6	eximii	|- E. y ( x C_ y /\ Tr y )
8	3 7	vtoclg	|- ( A e. V -> E. y ( A C_ y /\ Tr y ) )
9		ttcmin	|- ( ( A C_ y /\ Tr y ) -> TC+ A C_ y )
10		vex	|- y e. _V
11		ssexg	|- ( ( TC+ A C_ y /\ y e. _V ) -> TC+ A e. _V )
12	9 10 11	sylancl	|- ( ( A C_ y /\ Tr y ) -> TC+ A e. _V )
13	12	exlimiv	|- ( E. y ( A C_ y /\ Tr y ) -> TC+ A e. _V )
14	8 13	syl	|- ( A e. V -> TC+ A e. _V )