Definition df-tc 9495

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 9494	. 2 class TC
2		vx	. . 3 setvar 𝑥
3		cvv 3432	. . 3 class V
4	2	cv 1538	. . . . . . 7 class 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1538	. . . . . . 7 class 𝑦
7	4, 6	wss 3887	. . . . . 6 wff 𝑥 ⊆ 𝑦
8	6	wtr 5191	. . . . . 6 wff Tr 𝑦
9	7, 8	wa 396	. . . . 5 wff (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)
10	9, 5	cab 2715	. . . 4 class {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
11	10	cint 4879	. . 3 class ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
12	2, 3, 11	cmpt 5157	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
13	1, 12	wceq 1539	1 wff TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})

This definition is referenced by:  tcvalg  9496