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

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	⊢ 𝑋 = dom 𝐷
2	1	tailfval	⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) )
3	2	fveq1d	⊢ ( 𝐷 ∈ DirRel → ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) ‘ 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) ‘ 𝐴 ) )
5		id	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋 )
6		imaexg	⊢ ( 𝐷 ∈ DirRel → ( 𝐷 “ { 𝐴 } ) ∈ V )
7		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
8	7	imaeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐷 “ { 𝑥 } ) = ( 𝐷 “ { 𝐴 } ) )
9		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) )
10	8 9	fvmptg	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐷 “ { 𝐴 } ) ∈ V ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) ‘ 𝐴 ) = ( 𝐷 “ { 𝐴 } ) )
11	5 6 10	syl2anr	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 “ { 𝑥 } ) ) ‘ 𝐴 ) = ( 𝐷 “ { 𝐴 } ) )
12	4 11	eqtrd	⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝐴 ) = ( 𝐷 “ { 𝐴 } ) )