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	Could not format assertion : No typesetting found for |- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cttc	Could not format TC+ A : No typesetting found for class TC+ A with typecode class
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		cvv	$$class\mathrm{V}$$
5	3	cv	$$setvary$$
6	5	cuni	$$class\bigcup y$$
7	3 4 6	cmpt	$$class\left(y\in \mathrm{V}⟼\bigcup y\right)$$
8	2	cv	$$setvarx$$
9	8	csn	$$class\left\{x\right\}$$
10	7 9	crdg	$$class\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)$$
11		com	$$class\mathrm{\omega }$$
12	10 11	cima	$$class\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)\left[\mathrm{\omega }\right]$$
13	12	cuni	$$class\bigcup \mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)\left[\mathrm{\omega }\right]$$
14	2 0 13	ciun	$$class\bigcup _{x\in A}\bigcup \mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)\left[\mathrm{\omega }\right]$$
15	1 14	wceq	Could not format TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) : No typesetting found for wff TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) with typecode wff