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=\mathrm{Arrow}\left(C\right)$$
	arwdm.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	cdaf	$$⊢\left({{cod}_a\upharpoonright }_A\right):A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
2		arwdm.b	$$⊢B={\mathrm{Base}}_C$$
3		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
4		fofn	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 2^{nd}Fn\mathrm{V}$$
5	3 4	ax-mp	$$⊢2^{nd}Fn\mathrm{V}$$
6		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
7		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
8	6 7	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
9		fnfco	$$⊢\left(2^{nd}Fn\mathrm{V}\wedge 1^{st}:\mathrm{V}⟶\mathrm{V}\right)\to \left(2^{nd}\circ 1^{st}\right)Fn\mathrm{V}$$
10	5 8 9	mp2an	$$⊢\left(2^{nd}\circ 1^{st}\right)Fn\mathrm{V}$$
11		df-coda	$$⊢{cod}_a=2^{nd}\circ 1^{st}$$
12	11	fneq1i	$$⊢{cod}_{a}Fn\mathrm{V}\leftrightarrow \left(2^{nd}\circ 1^{st}\right)Fn\mathrm{V}$$
13	10 12	mpbir	$$⊢{cod}_{a}Fn\mathrm{V}$$
14		ssv	$$⊢A\subseteq \mathrm{V}$$
15		fnssres	$$⊢\left({cod}_{a}Fn\mathrm{V}\wedge A\subseteq \mathrm{V}\right)\to \left({{cod}_a\upharpoonright }_A\right)FnA$$
16	13 14 15	mp2an	$$⊢\left({{cod}_a\upharpoonright }_A\right)FnA$$
17		fvres	$$⊢x\in A\to \left({{cod}_a\upharpoonright }_A\right)\left(x\right)={cod}_a\left(x\right)$$
18	1 2	arwcd	$$⊢x\in A\to {cod}_a\left(x\right)\in B$$
19	17 18	eqeltrd	$$⊢x\in A\to \left({{cod}_a\upharpoonright }_A\right)\left(x\right)\in B$$
20	19	rgen	$$⊢\forall x\in A\left({{cod}_a\upharpoonright }_A\right)\left(x\right)\in B$$
21		ffnfv	$$⊢\left({{cod}_a\upharpoonright }_A\right):A⟶B\leftrightarrow \left(\left({{cod}_a\upharpoonright }_A\right)FnA\wedge \forall x\in A\left({{cod}_a\upharpoonright }_A\right)\left(x\right)\in B\right)$$
22	16 20 21	mpbir2an	$$⊢\left({{cod}_a\upharpoonright }_A\right):A⟶B$$