yonedalem3a

	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	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yonedalem3a.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
Assertion	yonedalem3a	⊢ ( 𝜑 → ( ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ∧ ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ) )

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		yonedalem3a.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
19		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
20	19	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) )
21		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → 𝑓 = 𝐹 )
22	20 21	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
23	19	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑋 ) )
24	19	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( 1 ‘ 𝑥 ) = ( 1 ‘ 𝑋 ) )
25	23 24	fveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) )
26	22 25	mpteq12dv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) → ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
27		ovex	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ∈ V
28	27	mptex	⊢ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ∈ V
29	26 18 28	ovmpoa	⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
30	16 17 29	syl2anc	⊢ ( 𝜑 → ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
31		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
33	31 32	nat1st2nd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
34	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
35		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
36	17	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑋 ∈ 𝐵 )
37	31 33 34 35 36	natcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
38	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
39	13 38	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑈 ∈ V )
41		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
42		relfunc	⊢ Rel ( 𝑂 Func 𝑆 )
43	1 2 12 17 4 5 39 14	yon1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )
44		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
45	42 43 44	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
46	34 41 45	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
47	46 17	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
48	5 39	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
49	47 48	eleqtrrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ∈ 𝑈 )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ∈ 𝑈 )
51		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ 𝐹 ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
52	42 16 51	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
53	34 41 52	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
54	53 17	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
55	54 48	eleqtrrd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
57	5 40 35 50 56	elsetchom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) ↔ ( 𝑎 ‘ 𝑋 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
58	37 57	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑋 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
59		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
60	2 59 3 12 17	catidcl	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
61	1 2 12 17 59 17	yon11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
62	60 61	eleqtrrd	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) )
64	58 63	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
65	64	fmpttd	⊢ ( 𝜑 → ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
66	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	yonedalem21	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
67	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
68	12 67	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
69	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
70	39 69	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
71	10 68 70 34 16 17	evlf1	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
72	30 66 71	feq123d	⊢ ( 𝜑 → ( ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ↔ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
73	65 72	mpbird	⊢ ( 𝜑 → ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) )
74	30 73	jca	⊢ ( 𝜑 → ( ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ∧ ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ) )

Metamath Proof Explorer

Theorem yonedalem3a

Proof