![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funcestrcsetc | Structured version Visualization version GIF version |
Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020.) |
Ref | Expression |
---|---|
funcestrcsetc.e | ⊢ 𝐸 = (ExtStrCat‘𝑈) |
funcestrcsetc.s | ⊢ 𝑆 = (SetCat‘𝑈) |
funcestrcsetc.b | ⊢ 𝐵 = (Base‘𝐸) |
funcestrcsetc.c | ⊢ 𝐶 = (Base‘𝑆) |
funcestrcsetc.u | ⊢ (𝜑 → 𝑈 ∈ WUni) |
funcestrcsetc.f | ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
funcestrcsetc.g | ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) |
Ref | Expression |
---|---|
funcestrcsetc | ⊢ (𝜑 → 𝐹(𝐸 Func 𝑆)𝐺) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funcestrcsetc.b | . 2 ⊢ 𝐵 = (Base‘𝐸) | |
2 | funcestrcsetc.c | . 2 ⊢ 𝐶 = (Base‘𝑆) | |
3 | eqid 2778 | . 2 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸) | |
4 | eqid 2778 | . 2 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆) | |
5 | eqid 2778 | . 2 ⊢ (Id‘𝐸) = (Id‘𝐸) | |
6 | eqid 2778 | . 2 ⊢ (Id‘𝑆) = (Id‘𝑆) | |
7 | eqid 2778 | . 2 ⊢ (comp‘𝐸) = (comp‘𝐸) | |
8 | eqid 2778 | . 2 ⊢ (comp‘𝑆) = (comp‘𝑆) | |
9 | funcestrcsetc.u | . . 3 ⊢ (𝜑 → 𝑈 ∈ WUni) | |
10 | funcestrcsetc.e | . . . 4 ⊢ 𝐸 = (ExtStrCat‘𝑈) | |
11 | 10 | estrccat 17244 | . . 3 ⊢ (𝑈 ∈ WUni → 𝐸 ∈ Cat) |
12 | 9, 11 | syl 17 | . 2 ⊢ (𝜑 → 𝐸 ∈ Cat) |
13 | funcestrcsetc.s | . . . 4 ⊢ 𝑆 = (SetCat‘𝑈) | |
14 | 13 | setccat 17206 | . . 3 ⊢ (𝑈 ∈ WUni → 𝑆 ∈ Cat) |
15 | 9, 14 | syl 17 | . 2 ⊢ (𝜑 → 𝑆 ∈ Cat) |
16 | funcestrcsetc.f | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) | |
17 | 10, 13, 1, 2, 9, 16 | funcestrcsetclem3 17253 | . 2 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) |
18 | funcestrcsetc.g | . . 3 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))) | |
19 | 10, 13, 1, 2, 9, 16, 18 | funcestrcsetclem4 17254 | . 2 ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) |
20 | 10, 13, 1, 2, 9, 16, 18 | funcestrcsetclem8 17258 | . 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝐸)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))) |
21 | 10, 13, 1, 2, 9, 16, 18 | funcestrcsetclem7 17257 | . 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘((Id‘𝐸)‘𝑎)) = ((Id‘𝑆)‘(𝐹‘𝑎))) |
22 | 10, 13, 1, 2, 9, 16, 18 | funcestrcsetclem9 17259 | . 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (ℎ ∈ (𝑎(Hom ‘𝐸)𝑏) ∧ 𝑘 ∈ (𝑏(Hom ‘𝐸)𝑐))) → ((𝑎𝐺𝑐)‘(𝑘(〈𝑎, 𝑏〉(comp‘𝐸)𝑐)ℎ)) = (((𝑏𝐺𝑐)‘𝑘)(〈(𝐹‘𝑎), (𝐹‘𝑏)〉(comp‘𝑆)(𝐹‘𝑐))((𝑎𝐺𝑏)‘ℎ))) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 12, 15, 17, 19, 20, 21, 22 | isfuncd 16996 | 1 ⊢ (𝜑 → 𝐹(𝐸 Func 𝑆)𝐺) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 class class class wbr 4930 ↦ cmpt 5009 I cid 5312 ↾ cres 5410 ‘cfv 6190 (class class class)co 6978 ∈ cmpo 6980 ↑𝑚 cmap 8208 WUnicwun 9922 Basecbs 16342 Hom chom 16435 compcco 16436 Catccat 16796 Idccid 16797 Func cfunc 16985 SetCatcsetc 17196 ExtStrCatcestrc 17233 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-uni 4714 df-int 4751 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-om 7399 df-1st 7503 df-2nd 7504 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-oadd 7911 df-er 8091 df-map 8210 df-ixp 8262 df-en 8309 df-dom 8310 df-sdom 8311 df-fin 8312 df-wun 9924 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-nn 11442 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-7 11511 df-8 11512 df-9 11513 df-n0 11711 df-z 11797 df-dec 11915 df-uz 12062 df-fz 12712 df-struct 16344 df-ndx 16345 df-slot 16346 df-base 16348 df-hom 16448 df-cco 16449 df-cat 16800 df-cid 16801 df-func 16989 df-setc 17197 df-estrc 17234 |
This theorem is referenced by: fthestrcsetc 17261 fullestrcsetc 17262 funcrngcsetc 43634 funcrngcsetcALT 43635 funcringcsetc 43671 |
Copyright terms: Public domain | W3C validator |