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 ⊢ T = C × c D
relxpchom.k ⊢ K = Hom ⁡ T
Assertion relxpchom ⊢ Rel ⁡ X K Y

Proof

Step Hyp Ref Expression
1 relxpchom.t ⊢ T = C × c D
2 relxpchom.k ⊢ K = Hom ⁡ T
3 xpss ⊢ 1 st ⁡ u Hom ⁡ C 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ D 2 nd ⁡ v ⊆ V × V
4 3 rgen2w ⊢ ∀ u ∈ Base T ∀ v ∈ Base T 1 st ⁡ u Hom ⁡ C 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ D 2 nd ⁡ v ⊆ V × V
5 eqid ⊢ Base T = Base T
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 eqid ⊢ Hom ⁡ D = Hom ⁡ D
8 1 5 6 7 2 xpchomfval ⊢ K = u ∈ Base T , v ∈ Base T ⟼ 1 st ⁡ u Hom ⁡ C 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ D 2 nd ⁡ v
9 8 ovmptss ⊢ ∀ u ∈ Base T ∀ v ∈ Base T 1 st ⁡ u Hom ⁡ C 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ D 2 nd ⁡ v ⊆ V × V → X K Y ⊆ V × V
10 4 9 ax-mp ⊢ X K Y ⊆ V × V
11 df-rel ⊢ Rel ⁡ X K Y ↔ X K Y ⊆ V × V
12 10 11 mpbir ⊢ Rel ⁡ X K Y