![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > funcringcsetcALTV2 | Structured version Visualization version GIF version |
Description: The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.) |
Ref | Expression |
---|---|
funcringcsetcALTV2.r | ⊢ 𝑅 = (RingCat‘𝑈) |
funcringcsetcALTV2.s | ⊢ 𝑆 = (SetCat‘𝑈) |
funcringcsetcALTV2.b | ⊢ 𝐵 = (Base‘𝑅) |
funcringcsetcALTV2.c | ⊢ 𝐶 = (Base‘𝑆) |
funcringcsetcALTV2.u | ⊢ (𝜑 → 𝑈 ∈ WUni) |
funcringcsetcALTV2.f | ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
funcringcsetcALTV2.g | ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) |
Ref | Expression |
---|---|
funcringcsetcALTV2 | ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funcringcsetcALTV2.b | . 2 ⊢ 𝐵 = (Base‘𝑅) | |
2 | funcringcsetcALTV2.c | . 2 ⊢ 𝐶 = (Base‘𝑆) | |
3 | eqid 2733 | . 2 ⊢ (Hom ‘𝑅) = (Hom ‘𝑅) | |
4 | eqid 2733 | . 2 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆) | |
5 | eqid 2733 | . 2 ⊢ (Id‘𝑅) = (Id‘𝑅) | |
6 | eqid 2733 | . 2 ⊢ (Id‘𝑆) = (Id‘𝑆) | |
7 | eqid 2733 | . 2 ⊢ (comp‘𝑅) = (comp‘𝑅) | |
8 | eqid 2733 | . 2 ⊢ (comp‘𝑆) = (comp‘𝑆) | |
9 | funcringcsetcALTV2.u | . . 3 ⊢ (𝜑 → 𝑈 ∈ WUni) | |
10 | funcringcsetcALTV2.r | . . . 4 ⊢ 𝑅 = (RingCat‘𝑈) | |
11 | 10 | ringccat 20661 | . . 3 ⊢ (𝑈 ∈ WUni → 𝑅 ∈ Cat) |
12 | 9, 11 | syl 17 | . 2 ⊢ (𝜑 → 𝑅 ∈ Cat) |
13 | funcringcsetcALTV2.s | . . . 4 ⊢ 𝑆 = (SetCat‘𝑈) | |
14 | 13 | setccat 18128 | . . 3 ⊢ (𝑈 ∈ WUni → 𝑆 ∈ Cat) |
15 | 9, 14 | syl 17 | . 2 ⊢ (𝜑 → 𝑆 ∈ Cat) |
16 | funcringcsetcALTV2.f | . . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) | |
17 | 10, 13, 1, 2, 9, 16 | funcringcsetcALTV2lem3 48053 | . 2 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) |
18 | funcringcsetcALTV2.g | . . 3 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) | |
19 | 10, 13, 1, 2, 9, 16, 18 | funcringcsetcALTV2lem4 48054 | . 2 ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) |
20 | 10, 13, 1, 2, 9, 16, 18 | funcringcsetcALTV2lem8 48058 | . 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑅)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏))) |
21 | 10, 13, 1, 2, 9, 16, 18 | funcringcsetcALTV2lem7 48057 | . 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘((Id‘𝑅)‘𝑎)) = ((Id‘𝑆)‘(𝐹‘𝑎))) |
22 | 10, 13, 1, 2, 9, 16, 18 | funcringcsetcALTV2lem9 48059 | . 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (ℎ ∈ (𝑎(Hom ‘𝑅)𝑏) ∧ 𝑘 ∈ (𝑏(Hom ‘𝑅)𝑐))) → ((𝑎𝐺𝑐)‘(𝑘(〈𝑎, 𝑏〉(comp‘𝑅)𝑐)ℎ)) = (((𝑏𝐺𝑐)‘𝑘)(〈(𝐹‘𝑎), (𝐹‘𝑏)〉(comp‘𝑆)(𝐹‘𝑐))((𝑎𝐺𝑏)‘ℎ))) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 12, 15, 17, 19, 20, 21, 22 | isfuncd 17905 | 1 ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1535 ∈ wcel 2104 class class class wbr 5149 ↦ cmpt 5232 I cid 5575 ↾ cres 5685 ‘cfv 6558 (class class class)co 7425 ∈ cmpo 7427 WUnicwun 10731 Basecbs 17234 Hom chom 17298 compcco 17299 Catccat 17698 Idccid 17699 Func cfunc 17894 SetCatcsetc 18118 RingHom crh 20471 RingCatcringc 20643 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4915 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7381 df-ov 7428 df-oprab 7429 df-mpo 7430 df-om 7881 df-1st 8007 df-2nd 8008 df-frecs 8299 df-wrecs 8330 df-recs 8404 df-rdg 8443 df-1o 8499 df-er 8738 df-map 8861 df-pm 8862 df-ixp 8931 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-wun 10733 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11485 df-neg 11486 df-nn 12258 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12518 df-z 12605 df-dec 12725 df-uz 12870 df-fz 13538 df-struct 17170 df-sets 17187 df-slot 17205 df-ndx 17217 df-base 17235 df-ress 17264 df-plusg 17300 df-hom 17311 df-cco 17312 df-0g 17477 df-cat 17702 df-cid 17703 df-homf 17704 df-ssc 17847 df-resc 17848 df-subc 17849 df-func 17898 df-setc 18119 df-estrc 18167 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-mhm 18794 df-grp 18952 df-ghm 19229 df-mgp 20138 df-ur 20185 df-ring 20238 df-rhm 20474 df-ringc 20644 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |