yon11

Description: Value of the Yoneda embedding at an object. 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	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	yon11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑍 ) = ( 𝑍 𝐻 𝑋 ) )

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		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
8		eqid	⊢ ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom_F ‘ ( oppCat ‘ 𝐶 ) )
9	1 3 7 8	yonval	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) = ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) )
12	11	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) = ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) )
13	12	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑍 ) = ( ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) ‘ 𝑍 ) )
14		eqid	⊢ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) )
15	7	oppccat	⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
16	3 15	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
17		eqid	⊢ ( SetCat ‘ ran ( Hom_f ‘ 𝐶 ) ) = ( SetCat ‘ ran ( Hom_f ‘ 𝐶 ) )
18		fvex	⊢ ( Hom_f ‘ 𝐶 ) ∈ V
19	18	rnex	⊢ ran ( Hom_f ‘ 𝐶 ) ∈ V
20	19	a1i	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ∈ V )
21		ssidd	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ ran ( Hom_f ‘ 𝐶 ) )
22	7 8 17 3 20 21	oppchofcl	⊢ ( 𝜑 → ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ∈ ( ( 𝐶 ×_c ( oppCat ‘ 𝐶 ) ) Func ( SetCat ‘ ran ( Hom_f ‘ 𝐶 ) ) ) )
23	7 2	oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
24		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 )
25	14 2 3 16 22 23 4 24 6	curf11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curry_F ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) ) ‘ 𝑋 ) ) ‘ 𝑍 ) = ( 𝑋 ( 1^st ‘ ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) 𝑍 ) )
26		eqid	⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
27	8 16 23 26 4 6	hof1	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) 𝑍 ) = ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑍 ) )
28	5 7	oppchom	⊢ ( 𝑋 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑍 ) = ( 𝑍 𝐻 𝑋 )
29	27 28	eqtrdi	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( Hom_F ‘ ( oppCat ‘ 𝐶 ) ) ) 𝑍 ) = ( 𝑍 𝐻 𝑋 ) )
30	13 25 29	3eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑍 ) = ( 𝑍 𝐻 𝑋 ) )

Metamath Proof Explorer

Theorem yon11

Proof