Definition df-tc 9173

Description: The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.)

Assertion

Ref	Expression
df-tc	⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-tc

Step	Hyp	Ref	Expression
1		ctc 9172	. 2 class TC
2		vx	. . 3 setvar 𝑥
3		cvv 3494	. . 3 class V
4	2	cv 1532	. . . . . . 7 class 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1532	. . . . . . 7 class 𝑦
7	4, 6	wss 3935	. . . . . 6 wff 𝑥 ⊆ 𝑦
8	6	wtr 5164	. . . . . 6 wff Tr 𝑦
9	7, 8	wa 398	. . . . 5 wff (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)
10	9, 5	cab 2799	. . . 4 class {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
11	10	cint 4868	. . 3 class ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
12	2, 3, 11	cmpt 5138	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
13	1, 12	wceq 1533	1 wff TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})

This definition is referenced by:  tcvalg  9174