Theorem oyoncl

Description: The opposite Yoneda embedding is a functor from oppCatC to the functor category C -> SetCat . (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	oyoncl.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oyoncl.y	⊢ 𝑌 = ( Yon ‘ 𝑂 )
	oyoncl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	oyoncl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	oyoncl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	oyoncl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
	oyoncl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝑆 )
Assertion	oyoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑂 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		oyoncl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝑆 )
8	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
9	3 8	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
10		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
11		eqid	⊢ ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 ) = ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 )
12		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
13	1 12	oppchomf	⊢ tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 )
14	13	rneqi	⊢ ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝑂 )
15		relxp	⊢ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
16		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
17	12 16	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
18	17	fndmi	⊢ dom ( Homf ‘ 𝐶 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
19	18	releqi	⊢ ( Rel dom ( Homf ‘ 𝐶 ) ↔ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
20	15 19	mpbir	⊢ Rel dom ( Homf ‘ 𝐶 )
21		rntpos	⊢ ( Rel dom ( Homf ‘ 𝐶 ) → ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝐶 ) )
22	20 21	ax-mp	⊢ ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝐶 )
23	14 22	eqtr3i	⊢ ran ( Homf ‘ 𝑂 ) = ran ( Homf ‘ 𝐶 )
24	23 6	eqsstrid	⊢ ( 𝜑 → ran ( Homf ‘ 𝑂 ) ⊆ 𝑈 )
25	2 9 10 4 11 5 24	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑂 Func ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 ) ) )
26	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
27	26	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
28	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
29	28	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
30		eqidd	⊢ ( 𝜑 → ( Homf ‘ 𝑆 ) = ( Homf ‘ 𝑆 ) )
31		eqidd	⊢ ( 𝜑 → ( compf ‘ 𝑆 ) = ( compf ‘ 𝑆 ) )
32	10	oppccat	⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
33	9 32	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ Cat )
34	4	setccat	⊢ ( 𝑈 ∈ 𝑉 → 𝑆 ∈ Cat )
35	5 34	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
36	27 29 30 31 3 33 35 35	fucpropd	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝑆 ) = ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 ) )
37	7 36	eqtrid	⊢ ( 𝜑 → 𝑄 = ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 ) )
38	37	oveq2d	⊢ ( 𝜑 → ( 𝑂 Func 𝑄 ) = ( 𝑂 Func ( ( oppCat ‘ 𝑂 ) FuncCat 𝑆 ) ) )
39	25 38	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑂 Func 𝑄 ) )