Theorem homarel

Description: An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion	homarel	⊢ Rel ( 𝑋 𝐻 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		xpss	⊢ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) ⊆ ( V × V )
3		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4	1	homarcl	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
5	1 3 4	homaf	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐻 : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ⟶ 𝒫 ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) )
6	1 3	homarcl2	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7	6	simpld	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
8	6	simprd	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
9	5 7 8	fovrnd	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 𝐻 𝑌 ) ∈ 𝒫 ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) )
10		elelpwi	⊢ ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑋 𝐻 𝑌 ) ∈ 𝒫 ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) ) → 𝑓 ∈ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) )
11	9 10	mpdan	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝑓 ∈ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) × V ) )
12	2 11	sselid	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → 𝑓 ∈ ( V × V ) )
13	12	ssriv	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ ( V × V )
14		df-rel	⊢ ( Rel ( 𝑋 𝐻 𝑌 ) ↔ ( 𝑋 𝐻 𝑌 ) ⊆ ( V × V ) )
15	13 14	mpbir	⊢ Rel ( 𝑋 𝐻 𝑌 )