Theorem homa1

Description: The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion	homa1	⊢ ( 𝑍 ( 𝑋 𝐻 𝑌 ) 𝐹 → 𝑍 = ⟨ 𝑋 , 𝑌 ⟩ )

Proof

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