Theorem cdaf

Description: The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	arwdm.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	cdaf	⊢ ( coda ↾ 𝐴 ) : 𝐴 ⟶ 𝐵

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2		arwdm.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		fo2nd	⊢ 2nd : V –onto→ V
4		fofn	⊢ ( 2nd : V –onto→ V → 2nd Fn V )
5	3 4	ax-mp	⊢ 2nd Fn V
6		fo1st	⊢ 1st : V –onto→ V
7		fof	⊢ ( 1st : V –onto→ V → 1st : V ⟶ V )
8	6 7	ax-mp	⊢ 1st : V ⟶ V
9		fnfco	⊢ ( ( 2nd Fn V ∧ 1st : V ⟶ V ) → ( 2nd ∘ 1st ) Fn V )
10	5 8 9	mp2an	⊢ ( 2nd ∘ 1st ) Fn V
11		df-coda	⊢ coda = ( 2nd ∘ 1st )
12	11	fneq1i	⊢ ( coda Fn V ↔ ( 2nd ∘ 1st ) Fn V )
13	10 12	mpbir	⊢ coda Fn V
14		ssv	⊢ 𝐴 ⊆ V
15		fnssres	⊢ ( ( coda Fn V ∧ 𝐴 ⊆ V ) → ( coda ↾ 𝐴 ) Fn 𝐴 )
16	13 14 15	mp2an	⊢ ( coda ↾ 𝐴 ) Fn 𝐴
17		fvres	⊢ ( 𝑥 ∈ 𝐴 → ( ( coda ↾ 𝐴 ) ‘ 𝑥 ) = ( coda ‘ 𝑥 ) )
18	1 2	arwcd	⊢ ( 𝑥 ∈ 𝐴 → ( coda ‘ 𝑥 ) ∈ 𝐵 )
19	17 18	eqeltrd	⊢ ( 𝑥 ∈ 𝐴 → ( ( coda ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 )
20	19	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ( ( coda ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵
21		ffnfv	⊢ ( ( coda ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ↔ ( ( coda ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( coda ↾ 𝐴 ) ‘ 𝑥 ) ∈ 𝐵 ) )
22	16 20 21	mpbir2an	⊢ ( coda ↾ 𝐴 ) : 𝐴 ⟶ 𝐵