Metamath Proof Explorer

Theorem tailval

Description: The tail of an element in a directed set. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Hypothesis tailfval.1 ⊢ X = dom ⁡ D
Assertion tailval ⊢ D ∈ DirRel ∧ A ∈ X → tail ⁡ D ⁡ A = D A

Proof

Step Hyp Ref Expression
1 tailfval.1 ⊢ X = dom ⁡ D
2 1 tailfval ⊢ D ∈ DirRel → tail ⁡ D = x ∈ X ⟼ D x
3 2 fveq1d ⊢ D ∈ DirRel → tail ⁡ D ⁡ A = x ∈ X ⟼ D x ⁡ A
4 3 adantr ⊢ D ∈ DirRel ∧ A ∈ X → tail ⁡ D ⁡ A = x ∈ X ⟼ D x ⁡ A
5 id ⊢ A ∈ X → A ∈ X
6 imaexg ⊢ D ∈ DirRel → D A ∈ V
7 sneq ⊢ x = A → x = A
8 7 imaeq2d ⊢ x = A → D x = D A
9 eqid ⊢ x ∈ X ⟼ D x = x ∈ X ⟼ D x
10 8 9 fvmptg ⊢ A ∈ X ∧ D A ∈ V → x ∈ X ⟼ D x ⁡ A = D A
11 5 6 10 syl2anr ⊢ D ∈ DirRel ∧ A ∈ X → x ∈ X ⟼ D x ⁡ A = D A
12 4 11 eqtrd ⊢ D ∈ DirRel ∧ A ∈ X → tail ⁡ D ⁡ A = D A