Definition df-tail

Description: Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009)

	Ref	Expression
Assertion	df-tail	$$⊢\mathrm{tail}=\left(r\in \mathrm{DirRel}⟼\left(x\in \bigcup \bigcup r⟼r\left[\left\{x\right\}\right]\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctail	$$class\mathrm{tail}$$
1		vr	$$setvarr$$
2		cdir	$$class\mathrm{DirRel}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarr$$
5	4	cuni	$$class\bigcup r$$
6	5	cuni	$$class\bigcup \bigcup r$$
7	3	cv	$$setvarx$$
8	7	csn	$$class\left\{x\right\}$$
9	4 8	cima	$$classr\left[\left\{x\right\}\right]$$
10	3 6 9	cmpt	$$class\left(x\in \bigcup \bigcup r⟼r\left[\left\{x\right\}\right]\right)$$
11	1 2 10	cmpt	$$class\left(r\in \mathrm{DirRel}⟼\left(x\in \bigcup \bigcup r⟼r\left[\left\{x\right\}\right]\right)\right)$$
12	0 11	wceq	$$wff\mathrm{tail}=\left(r\in \mathrm{DirRel}⟼\left(x\in \bigcup \bigcup r⟼r\left[\left\{x\right\}\right]\right)\right)$$