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	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yonffth.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yonffth.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yonffth.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yonffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yonffth.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	yonffth.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
Assertion	yonffth	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		yonffth.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yonffth.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3		yonffth.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
4		yonffth.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
5		yonffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		yonffth.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
7		yonffth.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10		eqid	⊢ ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ) = ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) )
11		eqid	⊢ ( HomF ‘ 𝑄 ) = ( HomF ‘ 𝑄 )
12		eqid	⊢ ( ( 𝑄 ×c 𝑂 ) FuncCat ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ) ) = ( ( 𝑄 ×c 𝑂 ) FuncCat ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ) )
13		eqid	⊢ ( 𝑂 evalF 𝑆 ) = ( 𝑂 evalF 𝑆 )
14		eqid	⊢ ( ( HomF ‘ 𝑄 ) ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) ) = ( ( HomF ‘ 𝑄 ) ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
15		fvex	⊢ ( Homf ‘ 𝑄 ) ∈ V
16	15	rnex	⊢ ran ( Homf ‘ 𝑄 ) ∈ V
17		unexg	⊢ ( ( ran ( Homf ‘ 𝑄 ) ∈ V ∧ 𝑈 ∈ 𝑉 ) → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ∈ V )
18	16 6 17	sylancr	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ∈ V )
19		ssidd	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) )
20		eqid	⊢ ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ∈ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
21		eqid	⊢ ( Inv ‘ ( ( 𝑄 ×c 𝑂 ) FuncCat ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ) ) ) = ( Inv ‘ ( ( 𝑄 ×c 𝑂 ) FuncCat ( SetCat ‘ ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ) ) )
22		eqid	⊢ ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ) = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
23	1 8 9 2 3 10 4 11 12 13 14 5 18 7 19 20 21 22	yonffthlem	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )