Definition df-tail

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

	Ref	Expression
Assertion	df-tail	|- tail = ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctail	|- tail
1		vr	|- r
2		cdir	|- DirRel
3		vx	|- x
4	1	cv	|- r
5	4	cuni	|- U. r
6	5	cuni	|- U. U. r
7	3	cv	|- x
8	7	csn	|- { x }
9	4 8	cima	|- ( r " { x } )
10	3 6 9	cmpt	|- ( x e. U. U. r |-> ( r " { x } ) )
11	1 2 10	cmpt	|- ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )
12	0 11	wceq	|- tail = ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )