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