Metamath Proof Explorer

Theorem yonffth

Description: The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category C as a full subcategory of the category Q of presheaves on C . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses yonffth.y ⊢ Y = Yon ⁡ C
yonffth.o ⊢ O = oppCat ⁡ C
yonffth.s ⊢ S = SetCat ⁡ U
yonffth.q ⊢ Q = O FuncCat S
yonffth.c ⊢ φ → C ∈ Cat
yonffth.u ⊢ φ → U ∈ V
yonffth.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
Assertion yonffth ⊢ φ → Y ∈ C Full Q ∩ C Faith Q

Proof

Step Hyp Ref Expression
1 yonffth.y ⊢ Y = Yon ⁡ C
2 yonffth.o ⊢ O = oppCat ⁡ C
3 yonffth.s ⊢ S = SetCat ⁡ U
4 yonffth.q ⊢ Q = O FuncCat S
5 yonffth.c ⊢ φ → C ∈ Cat
6 yonffth.u ⊢ φ → U ∈ V
7 yonffth.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
8 eqid ⊢ Base C = Base C
9 eqid ⊢ Id ⁡ C = Id ⁡ C
10 eqid ⊢ SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U = SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U
11 eqid ⊢ Hom F ⁡ Q = Hom F ⁡ Q
12 eqid ⊢ Q × c O FuncCat SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U = Q × c O FuncCat SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U
13 eqid ⊢ O eval F S = O eval F S
14 eqid ⊢ Hom F ⁡ Q ∘ func 1 st ⁡ Y tpos 2 nd ⁡ Y ∘ func Q 2 nd F O ⟨,⟩ F Q 1 st F O = Hom F ⁡ Q ∘ func 1 st ⁡ Y tpos 2 nd ⁡ Y ∘ func Q 2 nd F O ⟨,⟩ F Q 1 st F O
15 fvex ⊢ Hom 𝑓 ⁡ Q ∈ V
16 15 rnex ⊢ ran ⁡ Hom 𝑓 ⁡ Q ∈ V
17 unexg ⊢ ran ⁡ Hom 𝑓 ⁡ Q ∈ V ∧ U ∈ V → ran ⁡ Hom 𝑓 ⁡ Q ∪ U ∈ V
18 16 6 17 sylancr ⊢ φ → ran ⁡ Hom 𝑓 ⁡ Q ∪ U ∈ V
19 ssidd ⊢ φ → ran ⁡ Hom 𝑓 ⁡ Q ∪ U ⊆ ran ⁡ Hom 𝑓 ⁡ Q ∪ U
20 eqid ⊢ f ∈ O Func S , x ∈ Base C ⟼ a ∈ 1 st ⁡ Y ⁡ x O Nat S f ⟼ a ⁡ x ⁡ Id ⁡ C ⁡ x = f ∈ O Func S , x ∈ Base C ⟼ a ∈ 1 st ⁡ Y ⁡ x O Nat S f ⟼ a ⁡ x ⁡ Id ⁡ C ⁡ x
21 eqid ⊢ Inv ⁡ Q × c O FuncCat SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U = Inv ⁡ Q × c O FuncCat SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ Q ∪ U
22 eqid ⊢ f ∈ O Func S , x ∈ Base C ⟼ u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ Base C ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u = f ∈ O Func S , x ∈ Base C ⟼ u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ Base C ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u
23 1 8 9 2 3 10 4 11 12 13 14 5 18 7 19 20 21 22 yonffthlem ⊢ φ → Y ∈ C Full Q ∩ C Faith Q