Metamath Proof Explorer

Theorem funcringcsetcALTV

Description: The "natural forgetful functor" from the category of 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
Hypotheses funcringcsetcALTV.r ⊢ R = RingCatALTV ⁡ U
funcringcsetcALTV.s ⊢ S = SetCat ⁡ U
funcringcsetcALTV.b ⊢ B = Base R
funcringcsetcALTV.c ⊢ C = Base S
funcringcsetcALTV.u ⊢ φ → U ∈ WUni
funcringcsetcALTV.f ⊢ φ → F = x ∈ B ⟼ Base x
funcringcsetcALTV.g ⊢ φ → G = x ∈ B , y ∈ B ⟼ I ↾ x RingHom y
Assertion funcringcsetcALTV ⊢ φ → F R Func S G

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV.r ⊢ R = RingCatALTV ⁡ U
2 funcringcsetcALTV.s ⊢ S = SetCat ⁡ U
3 funcringcsetcALTV.b ⊢ B = Base R
4 funcringcsetcALTV.c ⊢ C = Base S
5 funcringcsetcALTV.u ⊢ φ → U ∈ WUni
6 funcringcsetcALTV.f ⊢ φ → F = x ∈ B ⟼ Base x
7 funcringcsetcALTV.g ⊢ φ → G = x ∈ B , y ∈ B ⟼ I ↾ x RingHom y
8 eqid ⊢ Hom ⁡ R = Hom ⁡ R
9 eqid ⊢ Hom ⁡ S = Hom ⁡ S
10 eqid ⊢ Id ⁡ R = Id ⁡ R
11 eqid ⊢ Id ⁡ S = Id ⁡ S
12 eqid ⊢ comp ⁡ R = comp ⁡ R
13 eqid ⊢ comp ⁡ S = comp ⁡ S
14 1 ringccatALTV ⊢ U ∈ WUni → R ∈ Cat
15 5 14 syl ⊢ φ → R ∈ Cat
16 2 setccat ⊢ U ∈ WUni → S ∈ Cat
17 5 16 syl ⊢ φ → S ∈ Cat
18 1 2 3 4 5 6 funcringcsetclem3ALTV ⊢ φ → F : B ⟶ C
19 1 2 3 4 5 6 7 funcringcsetclem4ALTV ⊢ φ → G Fn B × B
20 1 2 3 4 5 6 7 funcringcsetclem8ALTV ⊢ φ ∧ a ∈ B ∧ b ∈ B → a G b : a Hom ⁡ R b ⟶ F ⁡ a Hom ⁡ S F ⁡ b
21 1 2 3 4 5 6 7 funcringcsetclem7ALTV ⊢ φ ∧ a ∈ B → a G a ⁡ Id ⁡ R ⁡ a = Id ⁡ S ⁡ F ⁡ a
22 1 2 3 4 5 6 7 funcringcsetclem9ALTV ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B ∧ h ∈ a Hom ⁡ R b ∧ k ∈ b Hom ⁡ R c → a G c ⁡ k a b comp ⁡ R c h = b G c ⁡ k F ⁡ a F ⁡ b comp ⁡ S F ⁡ c a G b ⁡ h
23 3 4 8 9 10 11 12 13 15 17 18 19 20 21 22 isfuncd ⊢ φ → F R Func S G