Theorem relxpchom

Description: A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	relxpchom.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	relxpchom.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
Assertion	relxpchom	⊢ Rel ( 𝑋 𝐾 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		relxpchom.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		relxpchom.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
3		xpss	⊢ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V )
4	3	rgen2w	⊢ ∀ 𝑢 ∈ ( Base ‘ 𝑇 ) ∀ 𝑣 ∈ ( Base ‘ 𝑇 ) ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V )
5		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8	1 5 6 7 2	xpchomfval	⊢ 𝐾 = ( 𝑢 ∈ ( Base ‘ 𝑇 ) , 𝑣 ∈ ( Base ‘ 𝑇 ) ↦ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) )
9	8	ovmptss	⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑇 ) ∀ 𝑣 ∈ ( Base ‘ 𝑇 ) ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V ) → ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V ) )
10	4 9	ax-mp	⊢ ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V )
11		df-rel	⊢ ( Rel ( 𝑋 𝐾 𝑌 ) ↔ ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V ) )
12	10 11	mpbir	⊢ Rel ( 𝑋 𝐾 𝑌 )