Theorem oppcyon

Description: Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	oppcyon.o	|- O = ( oppCat ` C )
	oppcyon.y	|- Y = ( Yon ` O )
	oppcyon.m	|- M = ( HomF ` C )
	oppcyon.c	|- ( ph -> C e. Cat )
Assertion	oppcyon	|- ( ph -> Y = ( <. O , C >. curryF M ) )

Proof

Step	Hyp	Ref	Expression
1		oppcyon.o	|- O = ( oppCat ` C )
2		oppcyon.y	|- Y = ( Yon ` O )
3		oppcyon.m	|- M = ( HomF ` C )
4		oppcyon.c	|- ( ph -> C e. Cat )
5	1	2oppchomf	|- ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
6	5	a1i	|- ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
7	1	2oppccomf	|- ( comf ` C ) = ( comf ` ( oppCat ` O ) )
8	7	a1i	|- ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
9	1	oppccat	|- ( C e. Cat -> O e. Cat )
10	4 9	syl	|- ( ph -> O e. Cat )
11		eqid	|- ( oppCat ` O ) = ( oppCat ` O )
12	11	oppccat	|- ( O e. Cat -> ( oppCat ` O ) e. Cat )
13	10 12	syl	|- ( ph -> ( oppCat ` O ) e. Cat )
14	6 8 4 13	hofpropd	|- ( ph -> ( HomF ` C ) = ( HomF ` ( oppCat ` O ) ) )
15	3 14	eqtrid	|- ( ph -> M = ( HomF ` ( oppCat ` O ) ) )
16	15	oveq2d	|- ( ph -> ( <. O , ( oppCat ` O ) >. curryF M ) = ( <. O , ( oppCat ` O ) >. curryF ( HomF ` ( oppCat ` O ) ) ) )
17		eqidd	|- ( ph -> ( Homf ` O ) = ( Homf ` O ) )
18		eqidd	|- ( ph -> ( comf ` O ) = ( comf ` O ) )
19		eqid	|- ( SetCat ` ran ( Homf ` C ) ) = ( SetCat ` ran ( Homf ` C ) )
20		fvex	|- ( Homf ` C ) e. _V
21	20	rnex	|- ran ( Homf ` C ) e. _V
22	21	a1i	|- ( ph -> ran ( Homf ` C ) e. _V )
23		ssidd	|- ( ph -> ran ( Homf ` C ) C_ ran ( Homf ` C ) )
24	3 1 19 4 22 23	hofcl	|- ( ph -> M e. ( ( O Xc. C ) Func ( SetCat ` ran ( Homf ` C ) ) ) )
25	17 18 6 8 10 10 4 13 24	curfpropd	|- ( ph -> ( <. O , C >. curryF M ) = ( <. O , ( oppCat ` O ) >. curryF M ) )
26		eqid	|- ( HomF ` ( oppCat ` O ) ) = ( HomF ` ( oppCat ` O ) )
27	2 10 11 26	yonval	|- ( ph -> Y = ( <. O , ( oppCat ` O ) >. curryF ( HomF ` ( oppCat ` O ) ) ) )
28	16 25 27	3eqtr4rd	|- ( ph -> Y = ( <. O , C >. curryF M ) )