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} (C)$
	Assertion	homadmcd	$⊢ F \in (X H Y) \to F = ⟨X, Y, 2^{nd} (F)⟩$

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

Metamath Proof Explorer