Definition df-ttc 37245

Description: Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9720), 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 37284. (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 37244	. 2 class TC+ 𝐴
3		vx	. . 3 setvar 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5		cvv 3451	. . . . . . 7 class V
6	4	cv 1569	. . . . . . . 8 class 𝑦
7	6	cuni 4867	. . . . . . 7 class ∪ 𝑦
8	4, 5, 7	cmpt 5186	. . . . . 6 class (𝑦 ∈ V ↦ ∪ 𝑦)
9	3	cv 1569	. . . . . . 7 class 𝑥
10	9	csn 4584	. . . . . 6 class {𝑥}
11	8, 10	crdg 8401	. . . . 5 class rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥})
12		com 7866	. . . . 5 class ω
13	11, 12	cima 5654	. . . 4 class (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
14	13	cuni 4867	. . 3 class ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
15	3, 1, 14	ciun 4951	. 2 class ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
16	2, 15	wceq 1570	1 wff TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)

This definition is used by:  ttceq  37246  nfttc  37249  ttcid  37250  ttctr  37251  ttcmin  37254