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	|- ( domA |` A ) : A --> B

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		arwdm.b	|- B = ( Base ` C )
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 o. 1st ) Fn _V )
9	5 7 8	mp2an	|- ( 1st o. 1st ) Fn _V
10		df-doma	|- domA = ( 1st o. 1st )
11	10	fneq1i	|- ( domA Fn _V <-> ( 1st o. 1st ) Fn _V )
12	9 11	mpbir	|- domA Fn _V
13		ssv	|- A C_ _V
14		fnssres	|- ( ( domA Fn _V /\ A C_ _V ) -> ( domA |` A ) Fn A )
15	12 13 14	mp2an	|- ( domA |` A ) Fn A
16		fvres	|- ( x e. A -> ( ( domA |` A ) ` x ) = ( domA ` x ) )
17	1 2	arwdm	|- ( x e. A -> ( domA ` x ) e. B )
18	16 17	eqeltrd	|- ( x e. A -> ( ( domA |` A ) ` x ) e. B )
19	18	rgen	|- A. x e. A ( ( domA |` A ) ` x ) e. B
20		ffnfv	|- ( ( domA |` A ) : A --> B <-> ( ( domA |` A ) Fn A /\ A. x e. A ( ( domA |` A ) ` x ) e. B ) )
21	15 19 20	mpbir2an	|- ( domA |` A ) : A --> B