Theorem homadmcd

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

	Ref	Expression
Hypothesis	homahom.h	$$⊢H={Hom}_a\left(C\right)$$
Assertion	homadmcd	$$⊢F\in \left(XHY\right)\to F=⟨X,Y,2^{nd}\left(F\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		homahom.h	$$⊢H={Hom}_a\left(C\right)$$
2	1	homarel	$$⊢\mathrm{Rel}\left(XHY\right)$$
3		1st2nd	$$⊢\left(\mathrm{Rel}\left(XHY\right)\wedge F\in \left(XHY\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
4	2 3	mpan	$$⊢F\in \left(XHY\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
5		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(XHY\right)\wedge F\in \left(XHY\right)\right)\to 1^{st}\left(F\right)\left(XHY\right)2^{nd}\left(F\right)$$
6	2 5	mpan	$$⊢F\in \left(XHY\right)\to 1^{st}\left(F\right)\left(XHY\right)2^{nd}\left(F\right)$$
7	1	homa1	$$⊢1^{st}\left(F\right)\left(XHY\right)2^{nd}\left(F\right)\to 1^{st}\left(F\right)=⟨X,Y⟩$$
8	6 7	syl	$$⊢F\in \left(XHY\right)\to 1^{st}\left(F\right)=⟨X,Y⟩$$
9	8	opeq1d	$$⊢F\in \left(XHY\right)\to ⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩=⟨⟨X,Y⟩,2^{nd}\left(F\right)⟩$$
10	4 9	eqtrd	$$⊢F\in \left(XHY\right)\to F=⟨⟨X,Y⟩,2^{nd}\left(F\right)⟩$$
11		df-ot	$$⊢⟨X,Y,2^{nd}\left(F\right)⟩=⟨⟨X,Y⟩,2^{nd}\left(F\right)⟩$$
12	10 11	eqtr4di	$$⊢F\in \left(XHY\right)\to F=⟨X,Y,2^{nd}\left(F\right)⟩$$