Definition df-trcl

Description: Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011)

	Ref	Expression
Assertion	df-trcl	$$⊢\mathrm{t+}=\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge z\circ z\subseteq z\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctcl	$$class\mathrm{t+}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vz	$$setvarz$$
4	1	cv	$$setvarx$$
5	3	cv	$$setvarz$$
6	4 5	wss	$$wffx\subseteq z$$
7	5 5	ccom	$$class\left(z\circ z\right)$$
8	7 5	wss	$$wffz\circ z\subseteq z$$
9	6 8	wa	$$wff\left(x\subseteq z\wedge z\circ z\subseteq z\right)$$
10	9 3	cab	$$class\left\{z|\left(x\subseteq z\wedge z\circ z\subseteq z\right)\right\}$$
11	10	cint	$$class\bigcap \left\{z|\left(x\subseteq z\wedge z\circ z\subseteq z\right)\right\}$$
12	1 2 11	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge z\circ z\subseteq z\right)\right\}\right)$$
13	0 12	wceq	$$wff\mathrm{t+}=\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge z\circ z\subseteq z\right)\right\}\right)$$