Theorem tailini

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

	Ref	Expression
Hypothesis	tailini.1	$$⊢X=\mathrm{dom}D$$
Assertion	tailini	$$⊢\left(D\in \mathrm{DirRel}\wedge A\in X\right)\to A\in \mathrm{tail}\left(D\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		tailini.1	$$⊢X=\mathrm{dom}D$$
2	1	dirref	$$⊢\left(D\in \mathrm{DirRel}\wedge A\in X\right)\to ADA$$
3	1	eltail	$$⊢\left(D\in \mathrm{DirRel}\wedge A\in X\wedge A\in X\right)\to \left(A\in \mathrm{tail}\left(D\right)\left(A\right)\leftrightarrow ADA\right)$$
4	3	3anidm23	$$⊢\left(D\in \mathrm{DirRel}\wedge A\in X\right)\to \left(A\in \mathrm{tail}\left(D\right)\left(A\right)\leftrightarrow ADA\right)$$
5	2 4	mpbird	$$⊢\left(D\in \mathrm{DirRel}\wedge A\in X\right)\to A\in \mathrm{tail}\left(D\right)\left(A\right)$$