Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonedalem4b Structured version   Visualization version   GIF version

Theorem yonedalem4b 17521
 Description: Lemma for yoneda 17528. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
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
Ref Expression
yonedalem4b (𝜑 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦, 1   𝑢,𝑔,𝐴,𝑦   𝑢,𝑓,𝐶,𝑔,𝑥,𝑦   𝑓,𝐸,𝑔,𝑢,𝑦   𝑓,𝐹,𝑔,𝑢,𝑥,𝑦   𝐵,𝑓,𝑔,𝑢,𝑥,𝑦   𝑓,𝐺,𝑔,𝑥,𝑦   𝑓,𝑂,𝑔,𝑢,𝑥,𝑦   𝑆,𝑓,𝑔,𝑢,𝑥,𝑦   𝑄,𝑓,𝑔,𝑢,𝑥   𝑇,𝑓,𝑔,𝑢,𝑦   𝑃,𝑓,𝑔,𝑥,𝑦   𝜑,𝑓,𝑔,𝑢,𝑥,𝑦   𝑢,𝑅   𝑓,𝑌,𝑔,𝑢,𝑥,𝑦   𝑓,𝑍,𝑔,𝑢,𝑥,𝑦   𝑓,𝑋,𝑔,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑓)   𝑃(𝑢)   𝑄(𝑦)   𝑅(𝑥,𝑦,𝑓,𝑔)   𝑇(𝑥)   𝑈(𝑥,𝑦,𝑢,𝑓,𝑔)   1 (𝑢)   𝐸(𝑥)   𝐺(𝑢)   𝐻(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑁(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑊(𝑥,𝑦,𝑢,𝑓,𝑔)

Proof of Theorem yonedalem4b
StepHypRef Expression
1 yoneda.y . . . . 5 𝑌 = (Yon‘𝐶)
2 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
3 yoneda.1 . . . . 5 1 = (Id‘𝐶)
4 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
5 yoneda.s . . . . 5 𝑆 = (SetCat‘𝑈)
6 yoneda.t . . . . 5 𝑇 = (SetCat‘𝑉)
7 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
8 yoneda.h . . . . 5 𝐻 = (HomF𝑄)
9 yoneda.r . . . . 5 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
10 yoneda.e . . . . 5 𝐸 = (𝑂 evalF 𝑆)
11 yoneda.z . . . . 5 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
12 yoneda.c . . . . 5 (𝜑𝐶 ∈ Cat)
13 yoneda.w . . . . 5 (𝜑𝑉𝑊)
14 yoneda.u . . . . 5 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
15 yoneda.v . . . . 5 (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
16 yonedalem21.f . . . . 5 (𝜑𝐹 ∈ (𝑂 Func 𝑆))
17 yonedalem21.x . . . . 5 (𝜑𝑋𝐵)
18 yonedalem4.n . . . . 5 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
19 yonedalem4.p . . . . 5 (𝜑𝐴 ∈ ((1st𝐹)‘𝑋))
201, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19yonedalem4a 17520 . . . 4 (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))))
2120fveq1d 6651 . . 3 (𝜑 → (((𝐹𝑁𝑋)‘𝐴)‘𝑃) = ((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃))
2221fveq1d 6651 . 2 (𝜑 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑃)‘𝐺) = (((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺))
23 eqidd 2802 . . 3 (𝜑 → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))))
24 yonedalem4b.p . . . 4 (𝜑𝑃𝐵)
25 ovex 7172 . . . . . 6 (𝑦(Hom ‘𝐶)𝑋) ∈ V
2625mptex 6967 . . . . 5 (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)) ∈ V
2726a1i 11 . . . 4 ((𝜑𝑦 = 𝑃) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)) ∈ V)
28 yonedalem4b.g . . . . . . 7 (𝜑𝐺 ∈ (𝑃(Hom ‘𝐶)𝑋))
2928adantr 484 . . . . . 6 ((𝜑𝑦 = 𝑃) → 𝐺 ∈ (𝑃(Hom ‘𝐶)𝑋))
30 simpr 488 . . . . . . 7 ((𝜑𝑦 = 𝑃) → 𝑦 = 𝑃)
3130oveq1d 7154 . . . . . 6 ((𝜑𝑦 = 𝑃) → (𝑦(Hom ‘𝐶)𝑋) = (𝑃(Hom ‘𝐶)𝑋))
3229, 31eleqtrrd 2896 . . . . 5 ((𝜑𝑦 = 𝑃) → 𝐺 ∈ (𝑦(Hom ‘𝐶)𝑋))
33 fvexd 6664 . . . . 5 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴) ∈ V)
34 simplr 768 . . . . . . . 8 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → 𝑦 = 𝑃)
3534oveq2d 7155 . . . . . . 7 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → (𝑋(2nd𝐹)𝑦) = (𝑋(2nd𝐹)𝑃))
36 simpr 488 . . . . . . 7 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
3735, 36fveq12d 6656 . . . . . 6 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → ((𝑋(2nd𝐹)𝑦)‘𝑔) = ((𝑋(2nd𝐹)𝑃)‘𝐺))
3837fveq1d 6651 . . . . 5 (((𝜑𝑦 = 𝑃) ∧ 𝑔 = 𝐺) → (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴))
3932, 33, 38fvmptdv2 6767 . . . 4 ((𝜑𝑦 = 𝑃) → (((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)) → (((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴)))
40 nfmpt1 5131 . . . 4 𝑦(𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))
41 nffvmpt1 6660 . . . . . 6 𝑦((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)
42 nfcv 2958 . . . . . 6 𝑦𝐺
4341, 42nffv 6659 . . . . 5 𝑦(((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺)
4443nfeq1 2973 . . . 4 𝑦(((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴)
4524, 27, 39, 40, 44fvmptd2f 6765 . . 3 (𝜑 → ((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))) → (((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴)))
4623, 45mpd 15 . 2 (𝜑 → (((𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)))‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴))
4722, 46eqtrd 2836 1 (𝜑 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑃)‘𝐺) = (((𝑋(2nd𝐹)𝑃)‘𝐺)‘𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  Vcvv 3444   ∪ cun 3882   ⊆ wss 3884  ⟨cop 4534   ↦ cmpt 5113  ran crn 5524  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141  1st c1st 7673  2nd c2nd 7674  tpos ctpos 7878  Basecbs 16478  Hom chom 16571  Catccat 16930  Idccid 16931  Homf chomf 16932  oppCatcoppc 16976   Func cfunc 17119   ∘func ccofu 17121   FuncCat cfuc 17207  SetCatcsetc 17330   ×c cxpc 17413   1stF c1stf 17414   2ndF c2ndf 17415   ⟨,⟩F cprf 17416   evalF cevlf 17454  HomFchof 17493  Yoncyon 17494 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144 This theorem is referenced by:  yonedalem4c  17522  yonedainv  17526
 Copyright terms: Public domain W3C validator