Theorem homahom2

Description: The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homahom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
Assertion	homahom2	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 → 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		homahom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
3		df-br	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 ↔ ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	1	homarcl	⊢ ( ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
6	1 4	homarcl2	⊢ ( ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7	6	simpld	⊢ ( ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
8	6	simprd	⊢ ( ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
9	1 4 5 2 7 8	elhoma	⊢ ( ⟨ 𝑍 , 𝐹 ⟩ ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 ↔ ( 𝑍 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) ) ) )
10	3 9	sylbi	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 → ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 ↔ ( 𝑍 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) ) ) )
11	10	ibi	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 → ( 𝑍 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) ) )
12	11	simprd	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 → 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) )