Definition df-ttc 36675

Description: Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9645), this definition works even if 𝐴 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 36714. (Contributed by Matthew House, 6-Apr-2026.)

Assertion

Ref	Expression
df-ttc	⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)

Distinct variable group:   𝑥,𝐴,𝑦

Detailed syntax breakdown of Definition df-ttc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cttc 36674	. 2 class TC+ 𝐴
3		vx	. . 3 setvar 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5		cvv 3430	. . . . . . 7 class V
6	4	cv 1541	. . . . . . . 8 class 𝑦
7	6	cuni 4851	. . . . . . 7 class ∪ 𝑦
8	4, 5, 7	cmpt 5167	. . . . . 6 class (𝑦 ∈ V ↦ ∪ 𝑦)
9	3	cv 1541	. . . . . . 7 class 𝑥
10	9	csn 4568	. . . . . 6 class {𝑥}
11	8, 10	crdg 8339	. . . . 5 class rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥})
12		com 7808	. . . . 5 class ω
13	11, 12	cima 5625	. . . 4 class (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
14	13	cuni 4851	. . 3 class ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
15	3, 1, 14	ciun 4934	. 2 class ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
16	2, 15	wceq 1542	1 wff TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)

This definition is referenced by:  ttceq  36676  nfttc  36679  ttcid  36680  ttctr  36681  ttcmin  36684