Metamath Proof Explorer

Theorem tailfval

Description: The tail function for 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 tailfval ⊢ D ∈ DirRel → tail ⁡ D = x ∈ X ⟼ D x

Proof

Step Hyp Ref Expression
1 tailfval.1 ⊢ X = dom ⁡ D
2 uniexg ⊢ D ∈ DirRel → ⋃ D ∈ V
3 uniexg ⊢ ⋃ D ∈ V → ⋃ ⋃ D ∈ V
4 mptexg ⊢ ⋃ ⋃ D ∈ V → x ∈ ⋃ ⋃ D ⟼ D x ∈ V
5 2 3 4 3syl ⊢ D ∈ DirRel → x ∈ ⋃ ⋃ D ⟼ D x ∈ V
6 unieq ⊢ d = D → ⋃ d = ⋃ D
7 6 unieqd ⊢ d = D → ⋃ ⋃ d = ⋃ ⋃ D
8 imaeq1 ⊢ d = D → d x = D x
9 7 8 mpteq12dv ⊢ d = D → x ∈ ⋃ ⋃ d ⟼ d x = x ∈ ⋃ ⋃ D ⟼ D x
10 df-tail ⊢ tail = d ∈ DirRel ⟼ x ∈ ⋃ ⋃ d ⟼ d x
11 9 10 fvmptg ⊢ D ∈ DirRel ∧ x ∈ ⋃ ⋃ D ⟼ D x ∈ V → tail ⁡ D = x ∈ ⋃ ⋃ D ⟼ D x
12 5 11 mpdan ⊢ D ∈ DirRel → tail ⁡ D = x ∈ ⋃ ⋃ D ⟼ D x
13 dirdm ⊢ D ∈ DirRel → dom ⁡ D = ⋃ ⋃ D
14 1 13 syl5req ⊢ D ∈ DirRel → ⋃ ⋃ D = X
15 14 mpteq1d ⊢ D ∈ DirRel → x ∈ ⋃ ⋃ D ⟼ D x = x ∈ X ⟼ D x
16 12 15 eqtrd ⊢ D ∈ DirRel → tail ⁡ D = x ∈ X ⟼ D x