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	|- A = ( Arrow ` C )
	arwdm.b	|- B = ( Base ` C )
Assertion	cdaf	|- ( codA |` A ) : A --> B

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		arwdm.b	|- B = ( Base ` C )
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 o. 1st ) Fn _V )
10	5 8 9	mp2an	|- ( 2nd o. 1st ) Fn _V
11		df-coda	|- codA = ( 2nd o. 1st )
12	11	fneq1i	|- ( codA Fn _V <-> ( 2nd o. 1st ) Fn _V )
13	10 12	mpbir	|- codA Fn _V
14		ssv	|- A C_ _V
15		fnssres	|- ( ( codA Fn _V /\ A C_ _V ) -> ( codA |` A ) Fn A )
16	13 14 15	mp2an	|- ( codA |` A ) Fn A
17		fvres	|- ( x e. A -> ( ( codA |` A ) ` x ) = ( codA ` x ) )
18	1 2	arwcd	|- ( x e. A -> ( codA ` x ) e. B )
19	17 18	eqeltrd	|- ( x e. A -> ( ( codA |` A ) ` x ) e. B )
20	19	rgen	|- A. x e. A ( ( codA |` A ) ` x ) e. B
21		ffnfv	|- ( ( codA |` A ) : A --> B <-> ( ( codA |` A ) Fn A /\ A. x e. A ( ( codA |` A ) ` x ) e. B ) )
22	16 20 21	mpbir2an	|- ( codA |` A ) : A --> B