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

Metamath Proof Explorer

Theorem fnxpc

Description: The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Assertion fnxpc 
|- Xc. Fn ( _V X. _V )

Proof

Step Hyp Ref Expression
1 df-xpc 
 |-  Xc. = ( r e. _V , s e. _V |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b |-> ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
2 tpex 
 |-  { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V
3 2 csbex 
 |-  [_ ( u e. b , v e. b |-> ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V
4 3 csbex 
 |-  [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b |-> ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. _V
5 1 4 fnmpoi 
 |-  Xc. Fn ( _V X. _V )