homadmcd

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

		Ref	Expression
	Hypothesis	homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
	Assertion	homadmcd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ 𝑋 , 𝑌 , ( 2^nd ‘ 𝐹 ) ⟩ )

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
2	1	homarel	⊢ Rel ( 𝑋 𝐻 𝑌 )
3		1st2nd	⊢ ( ( Rel ( 𝑋 𝐻 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
4	2 3	mpan	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
5		1st2ndbr	⊢ ( ( Rel ( 𝑋 𝐻 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
6	2 5	mpan	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
7	1	homa1	⊢ ( ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) → ( 1^st ‘ 𝐹 ) = ⟨ 𝑋 , 𝑌 ⟩ )
8	6 7	syl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ 𝐹 ) = ⟨ 𝑋 , 𝑌 ⟩ )
9	8	opeq1d	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 2^nd ‘ 𝐹 ) ⟩ )
10	4 9	eqtrd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 2^nd ‘ 𝐹 ) ⟩ )
11		df-ot	⊢ ⟨ 𝑋 , 𝑌 , ( 2^nd ‘ 𝐹 ) ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 2^nd ‘ 𝐹 ) ⟩
12	10 11	eqtr4di	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ 𝑋 , 𝑌 , ( 2^nd ‘ 𝐹 ) ⟩ )

Metamath Proof Explorer