Definition df-ttc

Description: Transitive closure of a class. Unlike ( TCA ) (see df-tc ), this definition works even if A or its transitive closure is a proper class. Note that unless we assume Transitive Containment, the transitive closure of a set may be a proper class. If we only assume Regularity, then the class of sets whose transitive closure is a set is precisely the class of well-founded sets, see ttcwf3 . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	df-ttc	|- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cttc	|- TC+ A
2		vx	|- x
3		vy	|- y
4		cvv	|- _V
5	3	cv	|- y
6	5	cuni	|- U. y
7	3 4 6	cmpt	|- ( y e. _V |-> U. y )
8	2	cv	|- x
9	8	csn	|- { x }
10	7 9	crdg	|- rec ( ( y e. _V |-> U. y ) , { x } )
11		com	|- _om
12	10 11	cima	|- ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
13	12	cuni	|- U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
14	2 0 13	ciun	|- U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
15	1 14	wceq	|- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )