Theorem oyon1cl

Description: The opposite Yoneda embedding at an object of C is a functor from C to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	oyoncl.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oyoncl.y	⊢ 𝑌 = ( Yon ‘ 𝑂 )
	oyoncl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	oyoncl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	oyoncl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	oyoncl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
	oyon1cl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	oyon1cl.p	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	oyon1cl	⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝐶 Func 𝑆 ) )

Proof

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