Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > yonedalem1 | Structured version Visualization version GIF version |
Description: Lemma for yoneda 17763. (Contributed by Mario Carneiro, 28-Jan-2017.) |
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 ‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
Ref | Expression |
---|---|
yonedalem1 | ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | yoneda.z | . . 3 ⊢ 𝑍 = (𝐻 ∘func ((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) 〈,〉F (𝑄 1stF 𝑂))) | |
2 | eqid 2734 | . . . . 5 ⊢ ((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) 〈,〉F (𝑄 1stF 𝑂)) = ((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) 〈,〉F (𝑄 1stF 𝑂)) | |
3 | eqid 2734 | . . . . 5 ⊢ ((oppCat‘𝑄) ×c 𝑄) = ((oppCat‘𝑄) ×c 𝑄) | |
4 | eqid 2734 | . . . . . . 7 ⊢ (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂) | |
5 | yoneda.q | . . . . . . . 8 ⊢ 𝑄 = (𝑂 FuncCat 𝑆) | |
6 | yoneda.c | . . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ Cat) | |
7 | yoneda.o | . . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶) | |
8 | 7 | oppccat 17198 | . . . . . . . . 9 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
9 | 6, 8 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 𝑂 ∈ Cat) |
10 | yoneda.w | . . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑊) | |
11 | yoneda.v | . . . . . . . . . . 11 ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) | |
12 | 11 | unssbd 4092 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
13 | 10, 12 | ssexd 5206 | . . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ V) |
14 | yoneda.s | . . . . . . . . . 10 ⊢ 𝑆 = (SetCat‘𝑈) | |
15 | 14 | setccat 17563 | . . . . . . . . 9 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat) |
16 | 13, 15 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Cat) |
17 | 5, 9, 16 | fuccat 17451 | . . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ Cat) |
18 | eqid 2734 | . . . . . . 7 ⊢ (𝑄 2ndF 𝑂) = (𝑄 2ndF 𝑂) | |
19 | 4, 17, 9, 18 | 2ndfcl 17677 | . . . . . 6 ⊢ (𝜑 → (𝑄 2ndF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑂)) |
20 | eqid 2734 | . . . . . . . 8 ⊢ (oppCat‘𝑄) = (oppCat‘𝑄) | |
21 | relfunc 17340 | . . . . . . . . 9 ⊢ Rel (𝐶 Func 𝑄) | |
22 | yoneda.y | . . . . . . . . . 10 ⊢ 𝑌 = (Yon‘𝐶) | |
23 | yoneda.u | . . . . . . . . . 10 ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈) | |
24 | 22, 6, 7, 14, 5, 13, 23 | yoncl 17742 | . . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄)) |
25 | 1st2ndbr 7802 | . . . . . . . . 9 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) | |
26 | 21, 24, 25 | sylancr 590 | . . . . . . . 8 ⊢ (𝜑 → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
27 | 7, 20, 26 | funcoppc 17353 | . . . . . . 7 ⊢ (𝜑 → (1st ‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌)) |
28 | df-br 5044 | . . . . . . 7 ⊢ ((1st ‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌) ↔ 〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) | |
29 | 27, 28 | sylib 221 | . . . . . 6 ⊢ (𝜑 → 〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) |
30 | 19, 29 | cofucl 17366 | . . . . 5 ⊢ (𝜑 → (〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func (oppCat‘𝑄))) |
31 | eqid 2734 | . . . . . 6 ⊢ (𝑄 1stF 𝑂) = (𝑄 1stF 𝑂) | |
32 | 4, 17, 9, 31 | 1stfcl 17676 | . . . . 5 ⊢ (𝜑 → (𝑄 1stF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑄)) |
33 | 2, 3, 30, 32 | prfcl 17682 | . . . 4 ⊢ (𝜑 → ((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) 〈,〉F (𝑄 1stF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func ((oppCat‘𝑄) ×c 𝑄))) |
34 | yoneda.h | . . . . 5 ⊢ 𝐻 = (HomF‘𝑄) | |
35 | yoneda.t | . . . . 5 ⊢ 𝑇 = (SetCat‘𝑉) | |
36 | 11 | unssad 4091 | . . . . 5 ⊢ (𝜑 → ran (Homf ‘𝑄) ⊆ 𝑉) |
37 | 34, 20, 35, 17, 10, 36 | hofcl 17739 | . . . 4 ⊢ (𝜑 → 𝐻 ∈ (((oppCat‘𝑄) ×c 𝑄) Func 𝑇)) |
38 | 33, 37 | cofucl 17366 | . . 3 ⊢ (𝜑 → (𝐻 ∘func ((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉 ∘func (𝑄 2ndF 𝑂)) 〈,〉F (𝑄 1stF 𝑂))) ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
39 | 1, 38 | eqeltrid 2838 | . 2 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
40 | 35, 14, 10, 12 | funcsetcres2 17571 | . . 3 ⊢ (𝜑 → ((𝑄 ×c 𝑂) Func 𝑆) ⊆ ((𝑄 ×c 𝑂) Func 𝑇)) |
41 | yoneda.e | . . . 4 ⊢ 𝐸 = (𝑂 evalF 𝑆) | |
42 | 41, 5, 9, 16 | evlfcl 17702 | . . 3 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑆)) |
43 | 40, 42 | sseldd 3892 | . 2 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
44 | 39, 43 | jca 515 | 1 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 Vcvv 3401 ∪ cun 3855 ⊆ wss 3857 〈cop 4537 class class class wbr 5043 ran crn 5541 Rel wrel 5545 ‘cfv 6369 (class class class)co 7202 1st c1st 7748 2nd c2nd 7749 tpos ctpos 7956 Basecbs 16684 Catccat 17139 Idccid 17140 Homf chomf 17141 oppCatcoppc 17186 Func cfunc 17332 ∘func ccofu 17334 FuncCat cfuc 17421 SetCatcsetc 17553 ×c cxpc 17647 1stF c1stf 17648 2ndF c2ndf 17649 〈,〉F cprf 17650 evalF cevlf 17689 HomFchof 17728 Yoncyon 17729 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-iun 4896 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-om 7634 df-1st 7750 df-2nd 7751 df-tpos 7957 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-er 8380 df-map 8499 df-pm 8500 df-ixp 8568 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-7 11881 df-8 11882 df-9 11883 df-n0 12074 df-z 12160 df-dec 12277 df-uz 12422 df-fz 13079 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-hom 16791 df-cco 16792 df-cat 17143 df-cid 17144 df-homf 17145 df-comf 17146 df-oppc 17187 df-ssc 17287 df-resc 17288 df-subc 17289 df-func 17336 df-cofu 17338 df-nat 17422 df-fuc 17423 df-setc 17554 df-xpc 17651 df-1stf 17652 df-2ndf 17653 df-prf 17654 df-evlf 17693 df-curf 17694 df-hof 17730 df-yon 17731 |
This theorem is referenced by: yonedalem3b 17759 yonedalem3 17760 yonedainv 17761 yonffthlem 17762 yoneda 17763 |
Copyright terms: Public domain | W3C validator |