Theorem arwdm

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

	Ref	Expression
Hypotheses	arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	arwdm.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	arwdm	⊢ ( 𝐹 ∈ 𝐴 → ( doma ‘ 𝐹 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2		arwdm.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		eqid	⊢ ( Homa ‘ 𝐶 ) = ( Homa ‘ 𝐶 )
4	1 3	arwhoma	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ ( ( doma ‘ 𝐹 ) ( Homa ‘ 𝐶 ) ( coda ‘ 𝐹 ) ) )
5	3 2	homarcl2	⊢ ( 𝐹 ∈ ( ( doma ‘ 𝐹 ) ( Homa ‘ 𝐶 ) ( coda ‘ 𝐹 ) ) → ( ( doma ‘ 𝐹 ) ∈ 𝐵 ∧ ( coda ‘ 𝐹 ) ∈ 𝐵 ) )
6	4 5	syl	⊢ ( 𝐹 ∈ 𝐴 → ( ( doma ‘ 𝐹 ) ∈ 𝐵 ∧ ( coda ‘ 𝐹 ) ∈ 𝐵 ) )
7	6	simpld	⊢ ( 𝐹 ∈ 𝐴 → ( doma ‘ 𝐹 ) ∈ 𝐵 )