# Metamath Proof Explorer

## 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}↾}_{{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}↔\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}↾}_{{A}}\right)Fn{A}$
15 12 13 14 mp2an ${⊢}\left({{dom}_{a}↾}_{{A}}\right)Fn{A}$
16 fvres ${⊢}{x}\in {A}\to \left({{dom}_{a}↾}_{{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}↾}_{{A}}\right)\left({x}\right)\in {B}$
19 18 rgen ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({{dom}_{a}↾}_{{A}}\right)\left({x}\right)\in {B}$
20 ffnfv ${⊢}\left({{dom}_{a}↾}_{{A}}\right):{A}⟶{B}↔\left(\left({{dom}_{a}↾}_{{A}}\right)Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({{dom}_{a}↾}_{{A}}\right)\left({x}\right)\in {B}\right)$
21 15 19 20 mpbir2an ${⊢}\left({{dom}_{a}↾}_{{A}}\right):{A}⟶{B}$