Theorem yonedalem4b

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 ‘ 𝐹 ) ‘ 𝑋 ) )
	yonedalem4b.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	yonedalem4b.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
Assertion	yonedalem4b	⊢ ( 𝜑 → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 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		yonedalem4b.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
21		yonedalem4b.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	yonedalem4a	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
23	22	fveq1d	⊢ ( 𝜑 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑃 ) = ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) )
24	23	fveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 ) )
25		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
26		ovex	⊢ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ∈ V
27	26	mptex	⊢ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V
28	27	a1i	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V )
29	21	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → 𝐺 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → 𝑦 = 𝑃 )
31	30	oveq1d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
32	29 31	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → 𝐺 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) )
33		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ∈ V )
34		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → 𝑦 = 𝑃 )
35	34	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) )
36		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
37	35 36	fveq12d	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) )
38	37	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝑃 ) ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 ) )
39	32 33 38	fvmptdv2	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑃 ) → ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) → ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 ) ) )
40		nfmpt1	⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
41		nffvmpt1	⊢ Ⅎ 𝑦 ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 )
42		nfcv	⊢ Ⅎ 𝑦 𝐺
43	41 42	nffv	⊢ Ⅎ 𝑦 ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 )
44	43	nfeq1	⊢ Ⅎ 𝑦 ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 )
45	20 28 39 40 44	fvmptd2f	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) → ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 ) ) )
46	25 45	mpd	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 ) )
47	24 46	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑃 ) ‘ 𝐺 ) = ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐺 ) ‘ 𝐴 ) )