Theorem tailfval

Description: The tail function for a directed set. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Hypothesis	tailfval.1	|- X = dom D
Assertion	tailfval	|- ( D e. DirRel -> ( tail ` D ) = ( x e. X |-> ( D " { x } ) ) )

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	|- X = dom D
2		uniexg	|- ( D e. DirRel -> U. D e. _V )
3		uniexg	|- ( U. D e. _V -> U. U. D e. _V )
4		mptexg	|- ( U. U. D e. _V -> ( x e. U. U. D |-> ( D " { x } ) ) e. _V )
5	2 3 4	3syl	|- ( D e. DirRel -> ( x e. U. U. D |-> ( D " { x } ) ) e. _V )
6		unieq	|- ( d = D -> U. d = U. D )
7	6	unieqd	|- ( d = D -> U. U. d = U. U. D )
8		imaeq1	|- ( d = D -> ( d " { x } ) = ( D " { x } ) )
9	7 8	mpteq12dv	|- ( d = D -> ( x e. U. U. d |-> ( d " { x } ) ) = ( x e. U. U. D |-> ( D " { x } ) ) )
10		df-tail	|- tail = ( d e. DirRel |-> ( x e. U. U. d |-> ( d " { x } ) ) )
11	9 10	fvmptg	|- ( ( D e. DirRel /\ ( x e. U. U. D |-> ( D " { x } ) ) e. _V ) -> ( tail ` D ) = ( x e. U. U. D |-> ( D " { x } ) ) )
12	5 11	mpdan	|- ( D e. DirRel -> ( tail ` D ) = ( x e. U. U. D |-> ( D " { x } ) ) )
13		dirdm	|- ( D e. DirRel -> dom D = U. U. D )
14	1 13	eqtr2id	|- ( D e. DirRel -> U. U. D = X )
15	14	mpteq1d	|- ( D e. DirRel -> ( x e. U. U. D |-> ( D " { x } ) ) = ( x e. X |-> ( D " { x } ) ) )
16	12 15	eqtrd	|- ( D e. DirRel -> ( tail ` D ) = ( x e. X |-> ( D " { x } ) ) )