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+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cttc	⊢ TC+ 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		cvv	⊢ V
5	3	cv	⊢ 𝑦
6	5	cuni	⊢ ∪ 𝑦
7	3 4 6	cmpt	⊢ ( 𝑦 ∈ V ↦ ∪ 𝑦 )
8	2	cv	⊢ 𝑥
9	8	csn	⊢ { 𝑥 }
10	7 9	crdg	⊢ rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } )
11		com	⊢ ω
12	10 11	cima	⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
13	12	cuni	⊢ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
14	2 0 13	ciun	⊢ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
15	1 14	wceq	⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )