Definition df-tc 9717

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 9716	. 2 class TC
2		vx	. . 3 setvar 𝑥
3		cvv 3453	. . 3 class V
4	2	cv 1569	. . . . . . 7 class 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1569	. . . . . . 7 class 𝑦
7	4, 6	wss 3902	. . . . . 6 wff 𝑥 ⊆ 𝑦
8	6	wtr 5216	. . . . . 6 wff Tr 𝑦
9	7, 8	wa 401	. . . . 5 wff (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)
10	9, 5	cab 2740	. . . 4 class {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
11	10	cint 4910	. . 3 class ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
12	2, 3, 11	cmpt 5190	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
13	1, 12	wceq 1570	1 wff TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})

This definition is used by:  tcvalg  9718  dfttc3gw  37144