Theorem tailini

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

	Ref	Expression
Hypothesis	tailini.1	⊢ 𝑋 = dom 𝐷
Assertion	tailini	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tailini.1	⊢ 𝑋 = dom 𝐷
2	1	dirref	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 𝐷 𝐴 )
3	1	eltail	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐴 𝐷 𝐴 ) )
4	3	3anidm23	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐴 𝐷 𝐴 ) )
5	2 4	mpbird	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) )