Theorem oppcyon

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

	Ref	Expression
Hypotheses	oppcyon.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppcyon.y	⊢ 𝑌 = ( Yon ‘ 𝑂 )
	oppcyon.m	⊢ 𝑀 = ( HomF ‘ 𝐶 )
	oppcyon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion	oppcyon	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝑂 , 𝐶 ⟩ curryF 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcyon.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcyon.y	⊢ 𝑌 = ( Yon ‘ 𝑂 )
3		oppcyon.m	⊢ 𝑀 = ( HomF ‘ 𝐶 )
4		oppcyon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
6	5	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
7	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
8	7	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
9	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
10	4 9	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
11		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
12	11	oppccat	⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
13	10 12	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ Cat )
14	6 8 4 13	hofpropd	⊢ ( 𝜑 → ( HomF ‘ 𝐶 ) = ( HomF ‘ ( oppCat ‘ 𝑂 ) ) )
15	3 14	syl5eq	⊢ ( 𝜑 → 𝑀 = ( HomF ‘ ( oppCat ‘ 𝑂 ) ) )
16	15	oveq2d	⊢ ( 𝜑 → ( ⟨ 𝑂 , ( oppCat ‘ 𝑂 ) ⟩ curryF 𝑀 ) = ( ⟨ 𝑂 , ( oppCat ‘ 𝑂 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑂 ) ) ) )
17		eqidd	⊢ ( 𝜑 → ( Homf ‘ 𝑂 ) = ( Homf ‘ 𝑂 ) )
18		eqidd	⊢ ( 𝜑 → ( compf ‘ 𝑂 ) = ( compf ‘ 𝑂 ) )
19		eqid	⊢ ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) = ( SetCat ‘ ran ( Homf ‘ 𝐶 ) )
20		fvex	⊢ ( Homf ‘ 𝐶 ) ∈ V
21	20	rnex	⊢ ran ( Homf ‘ 𝐶 ) ∈ V
22	21	a1i	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ∈ V )
23		ssidd	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ ran ( Homf ‘ 𝐶 ) )
24	3 1 19 4 22 23	hofcl	⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑂 ×c 𝐶 ) Func ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) ) )
25	17 18 6 8 10 10 4 13 24	curfpropd	⊢ ( 𝜑 → ( ⟨ 𝑂 , 𝐶 ⟩ curryF 𝑀 ) = ( ⟨ 𝑂 , ( oppCat ‘ 𝑂 ) ⟩ curryF 𝑀 ) )
26		eqid	⊢ ( HomF ‘ ( oppCat ‘ 𝑂 ) ) = ( HomF ‘ ( oppCat ‘ 𝑂 ) )
27	2 10 11 26	yonval	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝑂 , ( oppCat ‘ 𝑂 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑂 ) ) ) )
28	16 25 27	3eqtr4rd	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝑂 , 𝐶 ⟩ curryF 𝑀 ) )