df-tc

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

		Ref	Expression
	Assertion	df-tc	$⊢ TC = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land Tr y)\})$

Step	Hyp	Ref	Expression
0		ctc	$class TC$
1		vx	$setvar x$
2		cvv	$class V$
3		vy	$setvar y$
4	1	cv	$setvar x$
5	3	cv	$setvar y$
6	4 5	wss	$wff x \subseteq y$
7	5	wtr	$wff Tr y$
8	6 7	wa	$wff (x \subseteq y \land Tr y)$
9	8 3	cab	$class \{y \| (x \subseteq y \land Tr y)\}$
10	9	cint	$class ⋂ \{y \| (x \subseteq y \land Tr y)\}$
11	1 2 10	cmpt	$class (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land Tr y)\})$
12	0 11	wceq	$wff TC = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land Tr y)\})$

Metamath Proof Explorer