Metamath Proof Explorer


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 DirRel A X tail D A = D A

Proof

Step Hyp Ref Expression
1 tailfval.1 X = dom D
2 1 tailfval D DirRel tail D = x X D x
3 2 fveq1d D DirRel tail D A = x X D x A
4 3 adantr D DirRel A X tail D A = x X D x A
5 id A X A X
6 imaexg D DirRel D A V
7 sneq x = A x = A
8 7 imaeq2d x = A D x = D A
9 eqid x X D x = x X D x
10 8 9 fvmptg A X D A V x X D x A = D A
11 5 6 10 syl2anr D DirRel A X x X D x A = D A
12 4 11 eqtrd D DirRel A X tail D A = D A