Theorem yon2

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

	Ref	Expression
Hypotheses	yon11.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yon11.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yon11.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yon11.p	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yon11.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	yon11.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	yon12.x	⊢ · = ( comp ‘ 𝐶 )
	yon12.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	yon2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑍 ) )
	yon2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑊 𝐻 𝑋 ) )
Assertion	yon2	⊢ ( 𝜑 → ( ( ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) ‘ 𝐺 ) = ( 𝐹 ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑍 ) 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		yon11.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yon11.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yon11.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		yon11.p	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		yon11.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
6		yon11.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		yon12.x	⊢ · = ( comp ‘ 𝐶 )
8		yon12.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9		yon2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑍 ) )
10		yon2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑊 𝐻 𝑋 ) )
11		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
12		eqid	⊢ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) = ( HomF ‘ ( oppCat ‘ 𝐶 ) )
13	1 3 11 12	yonval	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) )
14	13	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ 𝑌 ) = ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) )
15	14	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) = ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) )
16	15	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) ‘ 𝐹 ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) = ( ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) )
18		eqid	⊢ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) )
19	11	oppccat	⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
20	3 19	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
21		eqid	⊢ ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) = ( SetCat ‘ ran ( Homf ‘ 𝐶 ) )
22		fvex	⊢ ( Homf ‘ 𝐶 ) ∈ V
23	22	rnex	⊢ ran ( Homf ‘ 𝐶 ) ∈ V
24	23	a1i	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ∈ V )
25		ssidd	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ ran ( Homf ‘ 𝐶 ) )
26	11 12 21 3 24 25	oppchofcl	⊢ ( 𝜑 → ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ∈ ( ( 𝐶 ×c ( oppCat ‘ 𝐶 ) ) Func ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) ) )
27	11 2	oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
28		eqid	⊢ ( Id ‘ ( oppCat ‘ 𝐶 ) ) = ( Id ‘ ( oppCat ‘ 𝐶 ) )
29		eqid	⊢ ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) ‘ 𝐹 )
30	18 2 3 20 26 27 5 28 4 6 9 29 8	curf2val	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) = ( 𝐹 ( ⟨ 𝑋 , 𝑊 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ) )
31	17 30	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) = ( 𝐹 ( ⟨ 𝑋 , 𝑊 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ) )
32	31	fveq1d	⊢ ( 𝜑 → ( ( ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) ‘ 𝐺 ) = ( ( 𝐹 ( ⟨ 𝑋 , 𝑊 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ) ‘ 𝐺 ) )
33		eqid	⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
34		eqid	⊢ ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) )
35	5 11	oppchom	⊢ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑍 )
36	9 35	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
37	27 33 28 20 8	catidcl	⊢ ( 𝜑 → ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ∈ ( 𝑊 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) )
38	5 11	oppchom	⊢ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) = ( 𝑊 𝐻 𝑋 )
39	10 38	eleqtrrdi	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) )
40	12 20 27 33 4 8 6 8 34 36 37 39	hof2	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑊 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ) ‘ 𝐺 ) = ( ( ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐹 ) )
41	27 33 28 20 4 34 8 39	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) = 𝐺 )
42	41	oveq1d	⊢ ( 𝜑 → ( ( ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐹 ) )
43	2 7 11 6 4 8	oppcco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑍 ) 𝐺 ) )
44	42 43	eqtrd	⊢ ( 𝜑 → ( ( ( ( Id ‘ ( oppCat ‘ 𝐶 ) ) ‘ 𝑊 ) ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑍 ) 𝐺 ) )
45	32 40 44	3eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝑋 ( 2nd ‘ 𝑌 ) 𝑍 ) ‘ 𝐹 ) ‘ 𝑊 ) ‘ 𝐺 ) = ( 𝐹 ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑍 ) 𝐺 ) )