Metamath Proof Explorer

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 ∈ DirRel ∧ A ∈ X → A ∈ tail ⁡ D ⁡ A

Proof

Step Hyp Ref Expression
1 tailini.1 ⊢ X = dom ⁡ D
2 1 dirref ⊢ D ∈ DirRel ∧ A ∈ X → A D A
3 1 eltail ⊢ D ∈ DirRel ∧ A ∈ X ∧ A ∈ X → A ∈ tail ⁡ D ⁡ A ↔ A D A
4 3 3anidm23 ⊢ D ∈ DirRel ∧ A ∈ X → A ∈ tail ⁡ D ⁡ A ↔ A D A
5 2 4 mpbird ⊢ D ∈ DirRel ∧ A ∈ X → A ∈ tail ⁡ D ⁡ A