Theorem yon12

Description: Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (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	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	yon12.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 𝐻 𝑍 ) )
	yon12.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑋 ) )
Assertion	yon12	⊢ ( 𝜑 → ( ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) ‘ 𝐺 ) = ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) )

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		yon12.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 𝐻 𝑍 ) )
10		yon12.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑋 ) )
11		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
12		eqid	⊢ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) = ( HomF ‘ ( oppCat ‘ 𝐶 ) )
13	1 3 11 12	yonval	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) )
14	13	fveq2d	⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) = ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) = ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) )
17	16	oveqd	⊢ ( 𝜑 → ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) = ( 𝑍 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) 𝑊 ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) = ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) )
19		eqid	⊢ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) )
20	11	oppccat	⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
21	3 20	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
22		eqid	⊢ ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) = ( SetCat ‘ ran ( Homf ‘ 𝐶 ) )
23		fvex	⊢ ( Homf ‘ 𝐶 ) ∈ V
24	23	rnex	⊢ ran ( Homf ‘ 𝐶 ) ∈ V
25	24	a1i	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ∈ V )
26		ssidd	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ ran ( Homf ‘ 𝐶 ) )
27	11 12 22 3 25 26	oppchofcl	⊢ ( 𝜑 → ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ∈ ( ( 𝐶 ×c ( oppCat ‘ 𝐶 ) ) Func ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) ) )
28	11 2	oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
29		eqid	⊢ ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 )
30		eqid	⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
31		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
32	5 11	oppchom	⊢ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) = ( 𝑊 𝐻 𝑍 )
33	9 32	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) )
34	19 2 3 21 27 28 4 29 6 30 31 8 33	curf12	⊢ ( 𝜑 → ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑋 , 𝑊 ⟩ ) 𝐹 ) )
35	18 34	eqtrd	⊢ ( 𝜑 → ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑋 , 𝑊 ⟩ ) 𝐹 ) )
36	35	fveq1d	⊢ ( 𝜑 → ( ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) ‘ 𝐺 ) = ( ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑋 , 𝑊 ⟩ ) 𝐹 ) ‘ 𝐺 ) )
37		eqid	⊢ ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) )
38	2 5 31 3 4	catidcl	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
39	5 11	oppchom	⊢ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑋 )
40	38 39	eleqtrrdi	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
41	5 11	oppchom	⊢ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑍 ) = ( 𝑍 𝐻 𝑋 )
42	10 41	eleqtrrdi	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑍 ) )
43	12 21 28 30 4 6 4 8 37 40 33 42	hof2	⊢ ( 𝜑 → ( ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) ⟨ 𝑋 , 𝑊 ⟩ ) 𝐹 ) ‘ 𝐺 ) = ( ( 𝐹 ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
44	2 7 11 4 6 8	oppcco	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) = ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) )
45	44	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
46	2 7 11 4 4 8	oppcco	⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑋 ) ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) ) )
47	2 5 7 3 8 6 4 9 10	catcocl	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) ∈ ( 𝑊 𝐻 𝑋 ) )
48	2 5 31 3 8 7 4 47	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑊 , 𝑋 ⟩ · 𝑋 ) ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) ) = ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) )
49	45 46 48	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) 𝐺 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑊 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) )
50	36 43 49	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑍 ( 2nd ‘ ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝐹 ) ‘ 𝐺 ) = ( 𝐺 ( ⟨ 𝑊 , 𝑍 ⟩ · 𝑋 ) 𝐹 ) )