Definition df-tail

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

	Ref	Expression
Assertion	df-tail	⊢ tail = ( 𝑟 ∈ DirRel ↦ ( 𝑥 ∈ ∪ ∪ 𝑟 ↦ ( 𝑟 “ { 𝑥 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctail	⊢ tail
1		vr	⊢ 𝑟
2		cdir	⊢ DirRel
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑟
5	4	cuni	⊢ ∪ 𝑟
6	5	cuni	⊢ ∪ ∪ 𝑟
7	3	cv	⊢ 𝑥
8	7	csn	⊢ { 𝑥 }
9	4 8	cima	⊢ ( 𝑟 “ { 𝑥 } )
10	3 6 9	cmpt	⊢ ( 𝑥 ∈ ∪ ∪ 𝑟 ↦ ( 𝑟 “ { 𝑥 } ) )
11	1 2 10	cmpt	⊢ ( 𝑟 ∈ DirRel ↦ ( 𝑥 ∈ ∪ ∪ 𝑟 ↦ ( 𝑟 “ { 𝑥 } ) ) )
12	0 11	wceq	⊢ tail = ( 𝑟 ∈ DirRel ↦ ( 𝑥 ∈ ∪ ∪ 𝑟 ↦ ( 𝑟 “ { 𝑥 } ) ) )