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 Xc. D )
relxpchom.k 
|- K = ( Hom ` T )
Assertion relxpchom 
|- Rel ( X K Y )

Proof

Step Hyp Ref Expression
1 relxpchom.t 
 |-  T = ( C Xc. D )
2 relxpchom.k 
 |-  K = ( Hom ` T )
3 xpss 
 |-  ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) C_ ( _V X. _V )
4 3 rgen2w 
 |-  A. u e. ( Base ` T ) A. v e. ( Base ` T ) ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) C_ ( _V X. _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 e. ( Base ` T ) , v e. ( Base ` T ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) )
9 8 ovmptss 
 |-  ( A. u e. ( Base ` T ) A. v e. ( Base ` T ) ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) C_ ( _V X. _V ) -> ( X K Y ) C_ ( _V X. _V ) )
10 4 9 ax-mp 
 |-  ( X K Y ) C_ ( _V X. _V )
11 df-rel 
 |-  ( Rel ( X K Y ) <-> ( X K Y ) C_ ( _V X. _V ) )
12 10 11 mpbir 
 |-  Rel ( X K Y )