This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
arwdm.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion dmaf ( doma ↾ 𝐴 ) : 𝐴 ⟶ 𝐵

Proof

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