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 = Arrow ⁡ C
arwdm.b ⊢ B = Base C
Assertion dmaf ⊢ dom a ↾ A : A ⟶ B

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ A = Arrow ⁡ C
2 arwdm.b ⊢ B = Base C
3 fo1st ⊢ 1 st : V ⟶ onto V
4 fofn ⊢ 1 st : V ⟶ onto V → 1 st Fn V
5 3 4 ax-mp ⊢ 1 st Fn V
6 fof ⊢ 1 st : V ⟶ onto V → 1 st : V ⟶ V
7 3 6 ax-mp ⊢ 1 st : V ⟶ V
8 fnfco ⊢ 1 st Fn V ∧ 1 st : V ⟶ V → 1 st ∘ 1 st Fn V
9 5 7 8 mp2an ⊢ 1 st ∘ 1 st Fn V
10 df-doma ⊢ dom a = 1 st ∘ 1 st
11 10 fneq1i ⊢ dom a Fn V ↔ 1 st ∘ 1 st Fn V
12 9 11 mpbir ⊢ dom a Fn V
13 ssv ⊢ A ⊆ V
14 fnssres ⊢ dom a Fn V ∧ A ⊆ V → dom a ↾ A Fn A
15 12 13 14 mp2an ⊢ dom a ↾ A Fn A
16 fvres ⊢ x ∈ A → dom a ↾ A ⁡ x = dom a ⁡ x
17 1 2 arwdm ⊢ x ∈ A → dom a ⁡ x ∈ B
18 16 17 eqeltrd ⊢ x ∈ A → dom a ↾ A ⁡ x ∈ B
19 18 rgen ⊢ ∀ x ∈ A dom a ↾ A ⁡ x ∈ B
20 ffnfv ⊢ dom a ↾ A : A ⟶ B ↔ dom a ↾ A Fn A ∧ ∀ x ∈ A dom a ↾ A ⁡ x ∈ B
21 15 19 20 mpbir2an ⊢ dom a ↾ A : A ⟶ B