Metamath Proof Explorer


Theorem yon1cl

Description: The Yoneda embedding at an object of C is a presheaf on C , also known as 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 ( 𝜑𝑋𝐵 )
yon1cl.o 𝑂 = ( oppCat ‘ 𝐶 )
yon1cl.s 𝑆 = ( SetCat ‘ 𝑈 )
yon1cl.u ( 𝜑𝑈𝑉 )
yon1cl.h ( 𝜑 → ran ( Homf𝐶 ) ⊆ 𝑈 )
Assertion yon1cl ( 𝜑 → ( ( 1st𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )

Proof

Step Hyp Ref Expression
1 yon11.y 𝑌 = ( Yon ‘ 𝐶 )
2 yon11.b 𝐵 = ( Base ‘ 𝐶 )
3 yon11.c ( 𝜑𝐶 ∈ Cat )
4 yon11.p ( 𝜑𝑋𝐵 )
5 yon1cl.o 𝑂 = ( oppCat ‘ 𝐶 )
6 yon1cl.s 𝑆 = ( SetCat ‘ 𝑈 )
7 yon1cl.u ( 𝜑𝑈𝑉 )
8 yon1cl.h ( 𝜑 → ran ( Homf𝐶 ) ⊆ 𝑈 )
9 eqid ( 𝑂 FuncCat 𝑆 ) = ( 𝑂 FuncCat 𝑆 )
10 9 fucbas ( 𝑂 Func 𝑆 ) = ( Base ‘ ( 𝑂 FuncCat 𝑆 ) )
11 relfunc Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) )
12 1 3 5 6 9 7 8 yoncl ( 𝜑𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) )
13 1st2ndbr ( ( Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ∧ 𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ) → ( 1st𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd𝑌 ) )
14 11 12 13 sylancr ( 𝜑 → ( 1st𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd𝑌 ) )
15 2 10 14 funcf1 ( 𝜑 → ( 1st𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
16 15 4 ffvelrnd ( 𝜑 → ( ( 1st𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )