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

Metamath Proof Explorer

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

Proof

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