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	⊢ 𝑋 = dom 𝐷
Assertion	eltail	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐴 𝐷 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	⊢ 𝑋 = dom 𝐷
2	1	tailval	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) = ( 𝐷 “ { 𝐴 } ) )
3	2	eleq2d	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( 𝐷 “ { 𝐴 } ) ) )
4	3	3adant3	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( 𝐷 “ { 𝐴 } ) ) )
5		elimasng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( 𝐷 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐷 ) )
6		df-br	⊢ ( 𝐴 𝐷 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐷 )
7	5 6	bitr4di	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( 𝐷 “ { 𝐴 } ) ↔ 𝐴 𝐷 𝐵 ) )
8	7	3adant1	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( 𝐷 “ { 𝐴 } ) ↔ 𝐴 𝐷 𝐵 ) )
9	4 8	bitrd	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐵 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) ↔ 𝐴 𝐷 𝐵 ) )