Definition df-tc

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctc	⊢ TC
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	4 5	wss	⊢ 𝑥 ⊆ 𝑦
7	5	wtr	⊢ Tr 𝑦
8	6 7	wa	⊢ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 )
9	8 3	cab	⊢ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) }
10	9	cint	⊢ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) }
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
12	0 11	wceq	⊢ TC = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) } )