yonedalem21

	Ref	Expression
Hypotheses	yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
	yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
	yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
	yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	yonedalem21	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
4		yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
6		yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
7		yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
17		yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
18	11	fveq2i	⊢ ( 1^st ‘ 𝑍 ) = ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) )
19	18	oveqi	⊢ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( 𝐹 ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) 𝑋 )
20		df-ov	⊢ ( 𝐹 ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) 𝑋 ) = ( ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ )
21	19 20	eqtri	⊢ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ )
22		eqid	⊢ ( 𝑄 ×_c 𝑂 ) = ( 𝑄 ×_c 𝑂 )
23	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
24	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
25	22 23 24	xpcbas	⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×_c 𝑂 ) )
26		eqid	⊢ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) = ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) )
27		eqid	⊢ ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) = ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 )
28	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
29	12 28	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
30	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
31	13 30	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
32	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
33	31 32	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
34	7 29 33	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
35		eqid	⊢ ( 𝑄 2^nd_F 𝑂 ) = ( 𝑄 2^nd_F 𝑂 )
36	22 34 29 35	2ndfcl	⊢ ( 𝜑 → ( 𝑄 2^nd_F 𝑂 ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑂 ) )
37		eqid	⊢ ( oppCat ‘ 𝑄 ) = ( oppCat ‘ 𝑄 )
38		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
39	1 12 4 5 7 31 14	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
40		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
41	38 39 40	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
42	4 37 41	funcoppc	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2^nd ‘ 𝑌 ) )
43		df-br	⊢ ( ( 1^st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2^nd ‘ 𝑌 ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
44	42 43	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
45	36 44	cofucl	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func ( oppCat ‘ 𝑄 ) ) )
46		eqid	⊢ ( 𝑄 1^st_F 𝑂 ) = ( 𝑄 1^st_F 𝑂 )
47	22 34 29 46	1stfcl	⊢ ( 𝜑 → ( 𝑄 1^st_F 𝑂 ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑄 ) )
48	26 27 45 47	prfcl	⊢ ( 𝜑 → ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) ) )
49	15	unssad	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝑄 ) ⊆ 𝑉 )
50	8 37 6 34 13 49	hofcl	⊢ ( 𝜑 → 𝐻 ∈ ( ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) Func 𝑇 ) )
51	16 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝑋 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
52	25 48 50 51	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) )
53	21 52	syl5eq	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) )
54		eqid	⊢ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×_c 𝑂 ) )
55	26 25 54 45 47 51	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ⟩ )
56	25 36 44 51	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) )
57		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
58		fvex	⊢ ( 2^nd ‘ 𝑌 ) ∈ V
59	58	tposex	⊢ tpos ( 2^nd ‘ 𝑌 ) ∈ V
60	57 59	op1st	⊢ ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 )
61	60	a1i	⊢ ( 𝜑 → ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 ) )
62	22 25 54 34 29 35 51	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
63		op2ndg	⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
64	16 17 63	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
65	62 64	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
66	61 65	fveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) )
67	56 66	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) )
68	22 25 54 34 29 46 51	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
69		op1stg	⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
70	16 17 69	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
71	68 70	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
72	67 71	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ )
73	55 72	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ )
74	73	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) = ( ( 1^st ‘ 𝐻 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ) )
75		df-ov	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 1^st ‘ 𝐻 ) 𝐹 ) = ( ( 1^st ‘ 𝐻 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ )
76	74 75	syl6eqr	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 1^st ‘ 𝐻 ) 𝐹 ) )
77		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
78	7 77	fuchom	⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
79	1 2 12 17 4 5 31 14	yon1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )
80	8 34 23 78 79 16	hof1	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 1^st ‘ 𝐻 ) 𝐹 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
81	53 76 80	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )

Metamath Proof Explorer

Theorem yonedalem21

Proof