Theorem tailini

Description: A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009)

	Ref	Expression
Hypothesis	tailini.1	|- X = dom D
Assertion	tailini	|- ( ( D e. DirRel /\ A e. X ) -> A e. ( ( tail ` D ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		tailini.1	|- X = dom D
2	1	dirref	|- ( ( D e. DirRel /\ A e. X ) -> A D A )
3	1	eltail	|- ( ( D e. DirRel /\ A e. X /\ A e. X ) -> ( A e. ( ( tail ` D ) ` A ) <-> A D A ) )
4	3	3anidm23	|- ( ( D e. DirRel /\ A e. X ) -> ( A e. ( ( tail ` D ) ` A ) <-> A D A ) )
5	2 4	mpbird	|- ( ( D e. DirRel /\ A e. X ) -> A e. ( ( tail ` D ) ` A ) )