This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑋 𝐾 𝑌 )