Theorem arwdmcd

Description: Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	arwrcl.a	|- A = ( Arrow ` C )
Assertion	arwdmcd	|- ( F e. A -> F = <. ( domA ` F ) , ( codA ` F ) , ( 2nd ` F ) >. )

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		eqid	|- ( HomA ` C ) = ( HomA ` C )
3	1 2	arwhoma	|- ( F e. A -> F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) )
4	2	homadmcd	|- ( F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) -> F = <. ( domA ` F ) , ( codA ` F ) , ( 2nd ` F ) >. )
5	3 4	syl	|- ( F e. A -> F = <. ( domA ` F ) , ( codA ` F ) , ( 2nd ` F ) >. )