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 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵