Theorem funcringcsetcALTV2 48011

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.)

Hypotheses

Ref	Expression
funcringcsetcALTV2.r	⊢ 𝑅 = (RingCat‘𝑈)
funcringcsetcALTV2.s	⊢ 𝑆 = (SetCat‘𝑈)
funcringcsetcALTV2.b	⊢ 𝐵 = (Base‘𝑅)
funcringcsetcALTV2.c	⊢ 𝐶 = (Base‘𝑆)
funcringcsetcALTV2.u	⊢ (𝜑 → 𝑈 ∈ WUni)
funcringcsetcALTV2.f	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))
funcringcsetcALTV2.g	⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))

Assertion

Ref	Expression
funcringcsetcALTV2	⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)

Distinct variable groups:   𝑥,𝐵   𝜑,𝑥   𝑥,𝐶   𝑦,𝐵,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐶(𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem funcringcsetcALTV2

Dummy variables 𝑎 𝑏 𝑐 ℎ 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.b	. 2 ⊢ 𝐵 = (Base‘𝑅)
2		funcringcsetcALTV2.c	. 2 ⊢ 𝐶 = (Base‘𝑆)
3		eqid 2740	. 2 ⊢ (Hom ‘𝑅) = (Hom ‘𝑅)
4		eqid 2740	. 2 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
5		eqid 2740	. 2 ⊢ (Id‘𝑅) = (Id‘𝑅)
6		eqid 2740	. 2 ⊢ (Id‘𝑆) = (Id‘𝑆)
7		eqid 2740	. 2 ⊢ (comp‘𝑅) = (comp‘𝑅)
8		eqid 2740	. 2 ⊢ (comp‘𝑆) = (comp‘𝑆)
9		funcringcsetcALTV2.u	. . 3 ⊢ (𝜑 → 𝑈 ∈ WUni)
10		funcringcsetcALTV2.r	. . . 4 ⊢ 𝑅 = (RingCat‘𝑈)
11	10	ringccat 20679	. . 3 ⊢ (𝑈 ∈ WUni → 𝑅 ∈ Cat)
12	9, 11	syl 17	. 2 ⊢ (𝜑 → 𝑅 ∈ Cat)
13		funcringcsetcALTV2.s	. . . 4 ⊢ 𝑆 = (SetCat‘𝑈)
14	13	setccat 18146	. . 3 ⊢ (𝑈 ∈ WUni → 𝑆 ∈ Cat)
15	9, 14	syl 17	. 2 ⊢ (𝜑 → 𝑆 ∈ Cat)
16		funcringcsetcALTV2.f	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))
17	10, 13, 1, 2, 9, 16	funcringcsetcALTV2lem3 48004	. 2 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
18		funcringcsetcALTV2.g	. . 3 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))))
19	10, 13, 1, 2, 9, 16, 18	funcringcsetcALTV2lem4 48005	. 2 ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
20	10, 13, 1, 2, 9, 16, 18	funcringcsetcALTV2lem8 48009	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑅)𝑏)⟶((𝐹‘𝑎)(Hom ‘𝑆)(𝐹‘𝑏)))
21	10, 13, 1, 2, 9, 16, 18	funcringcsetcALTV2lem7 48008	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎𝐺𝑎)‘((Id‘𝑅)‘𝑎)) = ((Id‘𝑆)‘(𝐹‘𝑎)))
22	10, 13, 1, 2, 9, 16, 18	funcringcsetcALTV2lem9 48010	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (ℎ ∈ (𝑎(Hom ‘𝑅)𝑏) ∧ 𝑘 ∈ (𝑏(Hom ‘𝑅)𝑐))) → ((𝑎𝐺𝑐)‘(𝑘(⟨𝑎, 𝑏⟩(comp‘𝑅)𝑐)ℎ)) = (((𝑏𝐺𝑐)‘𝑘)(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩(comp‘𝑆)(𝐹‘𝑐))((𝑎𝐺𝑏)‘ℎ)))
23	1, 2, 3, 4, 5, 6, 7, 8, 12, 15, 17, 19, 20, 21, 22	isfuncd 17923	1 ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   class class class wbr 5166   ↦ cmpt 5249   I cid 5592   ↾ cres 5697  ‘cfv 6568  (class class class)co 7443   ∈ cmpo 7445  WUnicwun 10763  Basecbs 17252  Hom chom 17316  compcco 17317  Catccat 17716  Idccid 17717   Func cfunc 17912  SetCatcsetc 18136   RingHom crh 20489  RingCatcringc 20661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7764  ax-cnex 11234  ax-resscn 11235  ax-1cn 11236  ax-icn 11237  ax-addcl 11238  ax-addrcl 11239  ax-mulcl 11240  ax-mulrcl 11241  ax-mulcom 11242  ax-addass 11243  ax-mulass 11244  ax-distr 11245  ax-i2m1 11246  ax-1ne0 11247  ax-1rid 11248  ax-rnegex 11249  ax-rrecex 11250  ax-cnre 11251  ax-pre-lttri 11252  ax-pre-lttrn 11253  ax-pre-ltadd 11254  ax-pre-mulgt0 11255

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5650  df-we 5652  df-xp 5701  df-rel 5702  df-cnv 5703  df-co 5704  df-dm 5705  df-rn 5706  df-res 5707  df-ima 5708  df-pred 6327  df-ord 6393  df-on 6394  df-lim 6395  df-suc 6396  df-iota 6520  df-fun 6570  df-fn 6571  df-f 6572  df-f1 6573  df-fo 6574  df-f1o 6575  df-fv 6576  df-riota 7399  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7898  df-1st 8024  df-2nd 8025  df-frecs 8316  df-wrecs 8347  df-recs 8421  df-rdg 8460  df-1o 8516  df-er 8757  df-map 8880  df-pm 8881  df-ixp 8950  df-en 8998  df-dom 8999  df-sdom 9000  df-fin 9001  df-wun 10765  df-pnf 11320  df-mnf 11321  df-xr 11322  df-ltxr 11323  df-le 11324  df-sub 11516  df-neg 11517  df-nn 12288  df-2 12350  df-3 12351  df-4 12352  df-5 12353  df-6 12354  df-7 12355  df-8 12356  df-9 12357  df-n0 12548  df-z 12634  df-dec 12753  df-uz 12898  df-fz 13562  df-struct 17188  df-sets 17205  df-slot 17223  df-ndx 17235  df-base 17253  df-ress 17282  df-plusg 17318  df-hom 17329  df-cco 17330  df-0g 17495  df-cat 17720  df-cid 17721  df-homf 17722  df-ssc 17865  df-resc 17866  df-subc 17867  df-func 17916  df-setc 18137  df-estrc 18185  df-mgm 18672  df-sgrp 18751  df-mnd 18767  df-mhm 18812  df-grp 18970  df-ghm 19247  df-mgp 20156  df-ur 20203  df-ring 20256  df-rhm 20492  df-ringc 20662

This theorem is referenced by: (None)