Theorem tailval

Description: The tail of an element in 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	tailval	|- ( ( D e. DirRel /\ A e. X ) -> ( ( tail ` D ) ` A ) = ( D " { A } ) )

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	|- X = dom D
2	1	tailfval	|- ( D e. DirRel -> ( tail ` D ) = ( x e. X |-> ( D " { x } ) ) )
3	2	fveq1d	|- ( D e. DirRel -> ( ( tail ` D ) ` A ) = ( ( x e. X |-> ( D " { x } ) ) ` A ) )
4	3	adantr	|- ( ( D e. DirRel /\ A e. X ) -> ( ( tail ` D ) ` A ) = ( ( x e. X |-> ( D " { x } ) ) ` A ) )
5		id	|- ( A e. X -> A e. X )
6		imaexg	|- ( D e. DirRel -> ( D " { A } ) e. _V )
7		sneq	|- ( x = A -> { x } = { A } )
8	7	imaeq2d	|- ( x = A -> ( D " { x } ) = ( D " { A } ) )
9		eqid	|- ( x e. X |-> ( D " { x } ) ) = ( x e. X |-> ( D " { x } ) )
10	8 9	fvmptg	|- ( ( A e. X /\ ( D " { A } ) e. _V ) -> ( ( x e. X |-> ( D " { x } ) ) ` A ) = ( D " { A } ) )
11	5 6 10	syl2anr	|- ( ( D e. DirRel /\ A e. X ) -> ( ( x e. X |-> ( D " { x } ) ) ` A ) = ( D " { A } ) )
12	4 11	eqtrd	|- ( ( D e. DirRel /\ A e. X ) -> ( ( tail ` D ) ` A ) = ( D " { A } ) )