Theorem yonedalem4a

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-Jan-2017)

	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	⊢ 𝐻 = ( HomF ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
	yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yonedalem4.n	⊢ 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
	yonedalem4.p	⊢ ( 𝜑 → 𝐴 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) )
Assertion	yonedalem4a	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )

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	⊢ 𝐻 = ( HomF ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
17		yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
18		yonedalem4.n	⊢ 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
19		yonedalem4.p	⊢ ( 𝜑 → 𝐴 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) )
20	18	a1i	⊢ ( 𝜑 → 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ) )
21		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑓 = 𝐹 )
22	21	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) )
23		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑥 = 𝑋 )
24	22 23	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) )
25		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝑋 )
26	25	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) )
27		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑓 = 𝐹 )
28	27	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ 𝑓 ) = ( 2nd ‘ 𝐹 ) )
29		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = 𝑦 )
30	28 25 29	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) = ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) )
31	30	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) )
32	31	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) )
33	26 32	mpteq12dv	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) )
34	33	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) )
35	24 34	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( 𝑢 ∈ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) = ( 𝑢 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
36		fvex	⊢ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ∈ V
37	36	mptex	⊢ ( 𝑢 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ∈ V
38	37	a1i	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) ∈ V )
39	20 35 16 17 38	ovmpod	⊢ ( 𝜑 → ( 𝐹 𝑁 𝑋 ) = ( 𝑢 ∈ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
40		simpr	⊢ ( ( 𝜑 ∧ 𝑢 = 𝐴 ) → 𝑢 = 𝐴 )
41	40	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 = 𝐴 ) → ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) )
42	41	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑢 = 𝐴 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
43	42	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑢 = 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
44	2	fvexi	⊢ 𝐵 ∈ V
45	44	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ V
46	45	a1i	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ V )
47	39 43 19 46	fvmptd	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )