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	⊢ 𝑋 = dom 𝐷
Assertion	tailfval	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	⊢ 𝑋 = dom 𝐷
2		uniexg	⊢ ( 𝐷 ∈ DirRel → ∪ 𝐷 ∈ V )
3		uniexg	⊢ ( ∪ 𝐷 ∈ V → ∪ ∪ 𝐷 ∈ V )
4		mptexg	⊢ ( ∪ ∪ 𝐷 ∈ V → ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) ∈ V )
5	2 3 4	3syl	⊢ ( 𝐷 ∈ DirRel → ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) ∈ V )
6		unieq	⊢ ( 𝑑 = 𝐷 → ∪ 𝑑 = ∪ 𝐷 )
7	6	unieqd	⊢ ( 𝑑 = 𝐷 → ∪ ∪ 𝑑 = ∪ ∪ 𝐷 )
8		imaeq1	⊢ ( 𝑑 = 𝐷 → ( 𝑑 “ { 𝑥 } ) = ( 𝐷 “ { 𝑥 } ) )
9	7 8	mpteq12dv	⊢ ( 𝑑 = 𝐷 → ( 𝑥 ∈ ∪ ∪ 𝑑 ↦ ( 𝑑 “ { 𝑥 } ) ) = ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) )
10		df-tail	⊢ tail = ( 𝑑 ∈ DirRel ↦ ( 𝑥 ∈ ∪ ∪ 𝑑 ↦ ( 𝑑 “ { 𝑥 } ) ) )
11	9 10	fvmptg	⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) ∈ V ) → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) )
12	5 11	mpdan	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) )
13		dirdm	⊢ ( 𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷 )
14	1 13	eqtr2id	⊢ ( 𝐷 ∈ DirRel → ∪ ∪ 𝐷 = 𝑋 )
15	14	mpteq1d	⊢ ( 𝐷 ∈ DirRel → ( 𝑥 ∈ ∪ ∪ 𝐷 ↦ ( 𝐷 “ { 𝑥 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) )
16	12 15	eqtrd	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) )