Theorem dmaf

Description: The domain 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	dmaf	$$⊢\left({{dom}_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		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
4		fofn	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}Fn\mathrm{V}$$
5	3 4	ax-mp	$$⊢1^{st}Fn\mathrm{V}$$
6		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
7	3 6	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
8		fnfco	$$⊢\left(1^{st}Fn\mathrm{V}\wedge 1^{st}:\mathrm{V}⟶\mathrm{V}\right)\to \left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
9	5 7 8	mp2an	$$⊢\left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
10		df-doma	$$⊢{dom}_a=1^{st}\circ 1^{st}$$
11	10	fneq1i	$$⊢{dom}_{a}Fn\mathrm{V}\leftrightarrow \left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
12	9 11	mpbir	$$⊢{dom}_{a}Fn\mathrm{V}$$
13		ssv	$$⊢A\subseteq \mathrm{V}$$
14		fnssres	$$⊢\left({dom}_{a}Fn\mathrm{V}\wedge A\subseteq \mathrm{V}\right)\to \left({{dom}_a\upharpoonright }_A\right)FnA$$
15	12 13 14	mp2an	$$⊢\left({{dom}_a\upharpoonright }_A\right)FnA$$
16		fvres	$$⊢x\in A\to \left({{dom}_a\upharpoonright }_A\right)\left(x\right)={dom}_a\left(x\right)$$
17	1 2	arwdm	$$⊢x\in A\to {dom}_a\left(x\right)\in B$$
18	16 17	eqeltrd	$$⊢x\in A\to \left({{dom}_a\upharpoonright }_A\right)\left(x\right)\in B$$
19	18	rgen	$$⊢\forall x\in A\left({{dom}_a\upharpoonright }_A\right)\left(x\right)\in B$$
20		ffnfv	$$⊢\left({{dom}_a\upharpoonright }_A\right):A⟶B\leftrightarrow \left(\left({{dom}_a\upharpoonright }_A\right)FnA\wedge \forall x\in A\left({{dom}_a\upharpoonright }_A\right)\left(x\right)\in B\right)$$
21	15 19 20	mpbir2an	$$⊢\left({{dom}_a\upharpoonright }_A\right):A⟶B$$