Theorem xpcid

Description: The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	|- T = ( C Xc. D )
	xpccat.c	|- ( ph -> C e. Cat )
	xpccat.d	|- ( ph -> D e. Cat )
	xpccat.x	|- X = ( Base ` C )
	xpccat.y	|- Y = ( Base ` D )
	xpccat.i	|- I = ( Id ` C )
	xpccat.j	|- J = ( Id ` D )
	xpcid.1	|- .1. = ( Id ` T )
	xpcid.r	|- ( ph -> R e. X )
	xpcid.s	|- ( ph -> S e. Y )
Assertion	xpcid	|- ( ph -> ( .1. ` <. R , S >. ) = <. ( I ` R ) , ( J ` S ) >. )

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	|- T = ( C Xc. D )
2		xpccat.c	|- ( ph -> C e. Cat )
3		xpccat.d	|- ( ph -> D e. Cat )
4		xpccat.x	|- X = ( Base ` C )
5		xpccat.y	|- Y = ( Base ` D )
6		xpccat.i	|- I = ( Id ` C )
7		xpccat.j	|- J = ( Id ` D )
8		xpcid.1	|- .1. = ( Id ` T )
9		xpcid.r	|- ( ph -> R e. X )
10		xpcid.s	|- ( ph -> S e. Y )
11		df-ov	|- ( R .1. S ) = ( .1. ` <. R , S >. )
12	1 2 3 4 5 6 7	xpccatid	|- ( ph -> ( T e. Cat /\ ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) ) )
13	12	simprd	|- ( ph -> ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) )
14	8 13	syl5eq	|- ( ph -> .1. = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) )
15		simprl	|- ( ( ph /\ ( x = R /\ y = S ) ) -> x = R )
16	15	fveq2d	|- ( ( ph /\ ( x = R /\ y = S ) ) -> ( I ` x ) = ( I ` R ) )
17		simprr	|- ( ( ph /\ ( x = R /\ y = S ) ) -> y = S )
18	17	fveq2d	|- ( ( ph /\ ( x = R /\ y = S ) ) -> ( J ` y ) = ( J ` S ) )
19	16 18	opeq12d	|- ( ( ph /\ ( x = R /\ y = S ) ) -> <. ( I ` x ) , ( J ` y ) >. = <. ( I ` R ) , ( J ` S ) >. )
20		opex	|- <. ( I ` R ) , ( J ` S ) >. e. _V
21	20	a1i	|- ( ph -> <. ( I ` R ) , ( J ` S ) >. e. _V )
22	14 19 9 10 21	ovmpod	|- ( ph -> ( R .1. S ) = <. ( I ` R ) , ( J ` S ) >. )
23	11 22	syl5eqr	|- ( ph -> ( .1. ` <. R , S >. ) = <. ( I ` R ) , ( J ` S ) >. )