Theorem arwdm

Description: The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwrcl.a	|- A = ( Arrow ` C )
	arwdm.b	|- B = ( Base ` C )
Assertion	arwdm	|- ( F e. A -> ( domA ` F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		arwdm.b	|- B = ( Base ` C )
3		eqid	|- ( HomA ` C ) = ( HomA ` C )
4	1 3	arwhoma	|- ( F e. A -> F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) )
5	3 2	homarcl2	|- ( F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) -> ( ( domA ` F ) e. B /\ ( codA ` F ) e. B ) )
6	4 5	syl	|- ( F e. A -> ( ( domA ` F ) e. B /\ ( codA ` F ) e. B ) )
7	6	simpld	|- ( F e. A -> ( domA ` F ) e. B )