Metamath Proof Explorer

Theorem eltail

Description: An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Hypothesis tailfval.1 ⊢ X = dom ⁡ D
Assertion eltail ⊢ D ∈ DirRel ∧ A ∈ X ∧ B ∈ C → B ∈ tail ⁡ D ⁡ A ↔ A D B

Proof

Step Hyp Ref Expression
1 tailfval.1 ⊢ X = dom ⁡ D
2 1 tailval ⊢ D ∈ DirRel ∧ A ∈ X → tail ⁡ D ⁡ A = D A
3 2 eleq2d ⊢ D ∈ DirRel ∧ A ∈ X → B ∈ tail ⁡ D ⁡ A ↔ B ∈ D A
4 3 3adant3 ⊢ D ∈ DirRel ∧ A ∈ X ∧ B ∈ C → B ∈ tail ⁡ D ⁡ A ↔ B ∈ D A
5 elimasng ⊢ A ∈ X ∧ B ∈ C → B ∈ D A ↔ A B ∈ D
6 df-br ⊢ A D B ↔ A B ∈ D
7 5 6 bitr4di ⊢ A ∈ X ∧ B ∈ C → B ∈ D A ↔ A D B
8 7 3adant1 ⊢ D ∈ DirRel ∧ A ∈ X ∧ B ∈ C → B ∈ D A ↔ A D B
9 4 8 bitrd ⊢ D ∈ DirRel ∧ A ∈ X ∧ B ∈ C → B ∈ tail ⁡ D ⁡ A ↔ A D B