Theorem yoneda

Description: The Yoneda Lemma. There is a natural isomorphism between the functors Z and E , where Z ( F , X ) is the natural transformations from Yon ( X ) = Hom ( - , X ) to F , and E ( F , X ) = F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe U is used for forming the functor category Q = C ^op -> SetCat ( U ) , which itself does not (necessarily) live in U but instead is an element of the larger universe V . (If U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set U = V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
	yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
	yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoneda.h	⊢ 𝐻 = ( HomF ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yoneda.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
	yoneda.i	⊢ 𝐼 = ( Iso ‘ 𝑅 )
Assertion	yoneda	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐼 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
4		yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
6		yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
7		yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoneda.h	⊢ 𝐻 = ( HomF ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		yoneda.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
17		yoneda.i	⊢ 𝐼 = ( Iso ‘ 𝑅 )
18	9	fucbas	⊢ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) = ( Base ‘ 𝑅 )
19		eqid	⊢ ( Inv ‘ 𝑅 ) = ( Inv ‘ 𝑅 )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) )
21	20	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
22		funcrcl	⊢ ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) → ( ( 𝑄 ×c 𝑂 ) ∈ Cat ∧ 𝑇 ∈ Cat ) )
23	21 22	syl	⊢ ( 𝜑 → ( ( 𝑄 ×c 𝑂 ) ∈ Cat ∧ 𝑇 ∈ Cat ) )
24	23	simpld	⊢ ( 𝜑 → ( 𝑄 ×c 𝑂 ) ∈ Cat )
25	23	simprd	⊢ ( 𝜑 → 𝑇 ∈ Cat )
26	9 24 25	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
27	20	simprd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
28		eqid	⊢ ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ) = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 28	yonedainv	⊢ ( 𝜑 → 𝑀 ( 𝑍 ( Inv ‘ 𝑅 ) 𝐸 ) ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ) )
30	18 19 26 21 27 17 29	inviso1	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐼 𝐸 ) )