Theorem oppccofval

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcco.b	|- B = ( Base ` C )
	oppcco.c	|- .x. = ( comp ` C )
	oppcco.o	|- O = ( oppCat ` C )
	oppcco.x	|- ( ph -> X e. B )
	oppcco.y	|- ( ph -> Y e. B )
	oppcco.z	|- ( ph -> Z e. B )
Assertion	oppccofval	|- ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		oppcco.b	|- B = ( Base ` C )
2		oppcco.c	|- .x. = ( comp ` C )
3		oppcco.o	|- O = ( oppCat ` C )
4		oppcco.x	|- ( ph -> X e. B )
5		oppcco.y	|- ( ph -> Y e. B )
6		oppcco.z	|- ( ph -> Z e. B )
7		elfvex	|- ( X e. ( Base ` C ) -> C e. _V )
8	7 1	eleq2s	|- ( X e. B -> C e. _V )
9		eqid	|- ( Hom ` C ) = ( Hom ` C )
10	1 9 2 3	oppcval	|- ( C e. _V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
11	4 8 10	3syl	|- ( ph -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
12	11	fveq2d	|- ( ph -> ( comp ` O ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) ) )
13		ovex	|- ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) e. _V
14	1	fvexi	|- B e. _V
15	14 14	xpex	|- ( B X. B ) e. _V
16	15 14	mpoex	|- ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) e. _V
17		ccoid	|- comp = Slot ( comp ` ndx )
18	17	setsid	|- ( ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) e. _V /\ ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) e. _V ) -> ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) ) )
19	13 16 18	mp2an	|- ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
20	12 19	eqtr4di	|- ( ph -> ( comp ` O ) = ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) )
21		simprr	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> z = Z )
22		simprl	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> u = <. X , Y >. )
23	22	fveq2d	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` u ) = ( 2nd ` <. X , Y >. ) )
24	5	adantr	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> Y e. B )
25		op2ndg	|- ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
26	4 24 25	syl2an2r	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
27	23 26	eqtrd	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` u ) = Y )
28	21 27	opeq12d	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> <. z , ( 2nd ` u ) >. = <. Z , Y >. )
29	22	fveq2d	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` u ) = ( 1st ` <. X , Y >. ) )
30		op1stg	|- ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
31	4 24 30	syl2an2r	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` <. X , Y >. ) = X )
32	29 31	eqtrd	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` u ) = X )
33	28 32	oveq12d	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) = ( <. Z , Y >. .x. X ) )
34	33	tposeqd	|- ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) = tpos ( <. Z , Y >. .x. X ) )
35	4 5	opelxpd	|- ( ph -> <. X , Y >. e. ( B X. B ) )
36		ovex	|- ( <. Z , Y >. .x. X ) e. _V
37	36	tposex	|- tpos ( <. Z , Y >. .x. X ) e. _V
38	37	a1i	|- ( ph -> tpos ( <. Z , Y >. .x. X ) e. _V )
39	20 34 35 6 38	ovmpod	|- ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )