Theorem yonval

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

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

Proof

Step	Hyp	Ref	Expression
1		yonval.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yonval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		yonval.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
4		yonval.m	⊢ 𝑀 = ( HomF ‘ 𝑂 )
5		df-yon	⊢ Yon = ( 𝑐 ∈ Cat ↦ ( ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑐 ) ) ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → 𝑐 = 𝐶 )
7	6	fveq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝐶 ) )
8	7 3	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( oppCat ‘ 𝑐 ) = 𝑂 )
9	6 8	opeq12d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ = ⟨ 𝐶 , 𝑂 ⟩ )
10	8	fveq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( HomF ‘ ( oppCat ‘ 𝑐 ) ) = ( HomF ‘ 𝑂 ) )
11	10 4	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( HomF ‘ ( oppCat ‘ 𝑐 ) ) = 𝑀 )
12	9 11	oveq12d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑐 ) ) ) = ( ⟨ 𝐶 , 𝑂 ⟩ curryF 𝑀 ) )
13		ovexd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝑂 ⟩ curryF 𝑀 ) ∈ V )
14	5 12 2 13	fvmptd2	⊢ ( 𝜑 → ( Yon ‘ 𝐶 ) = ( ⟨ 𝐶 , 𝑂 ⟩ curryF 𝑀 ) )
15	1 14	eqtrid	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝐶 , 𝑂 ⟩ curryF 𝑀 ) )