Definition df-tc 8496

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 8495	. 2 class TC
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . . . 7 class 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1474	. . . . . . 7 class 𝑦
7	4, 6	wss 3540	. . . . . 6 wff 𝑥 ⊆ 𝑦
8	6	wtr 4680	. . . . . 6 wff Tr 𝑦
9	7, 8	wa 383	. . . . 5 wff (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)
10	9, 5	cab 2596	. . . 4 class {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
11	10	cint 4410	. . 3 class ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}
12	2, 3, 11	cmpt 4643	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
13	1, 12	wceq 1475	1 wff TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})

This definition is referenced by:  tcvalg  8497