# Metamath Proof Explorer

## Theorem funcringcsetc

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, 26-Mar-2020)

Ref Expression
Hypotheses funcringcsetc.r 𝑅 = ( RingCat ‘ 𝑈 )
funcringcsetc.s 𝑆 = ( SetCat ‘ 𝑈 )
funcringcsetc.b 𝐵 = ( Base ‘ 𝑅 )
funcringcsetc.u ( 𝜑𝑈 ∈ WUni )
funcringcsetc.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcringcsetc.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
Assertion funcringcsetc ( 𝜑𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

### Proof

Step Hyp Ref Expression
1 funcringcsetc.r 𝑅 = ( RingCat ‘ 𝑈 )
2 funcringcsetc.s 𝑆 = ( SetCat ‘ 𝑈 )
3 funcringcsetc.b 𝐵 = ( Base ‘ 𝑅 )
4 funcringcsetc.u ( 𝜑𝑈 ∈ WUni )
5 funcringcsetc.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
6 funcringcsetc.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
7 eqid ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
8 eqid ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) )
9 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 7 4 estrcbas ( 𝜑𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) )
11 10 mpteq1d ( 𝜑 → ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( Base ‘ 𝑥 ) ) )
12 mpoeq12 ( ( 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ∧ 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑦 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
13 10 10 12 syl2anc ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑦 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
14 7 2 8 9 4 11 13 funcestrcsetc ( 𝜑 → ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
15 df-br ( ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ↔ ⟨ ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
16 14 15 sylib ( 𝜑 → ⟨ ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
17 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 1 17 4 ringcbas ( 𝜑 → ( Base ‘ 𝑅 ) = ( 𝑈 ∩ Ring ) )
19 incom ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 )
20 18 19 syl6eq ( 𝜑 → ( Base ‘ 𝑅 ) = ( Ring ∩ 𝑈 ) )
21 eqid ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
22 1 17 4 21 ringchomfval ( 𝜑 → ( Hom ‘ 𝑅 ) = ( RingHom ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
23 7 4 20 22 rhmsubcsetc ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
24 16 23 funcres ( 𝜑 → ( ⟨ ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾f ( Hom ‘ 𝑅 ) ) ∈ ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func 𝑆 ) )
25 mptexg ( 𝑈 ∈ WUni → ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ∈ V )
26 4 25 syl ( 𝜑 → ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ∈ V )
27 fvex ( Hom ‘ 𝑅 ) ∈ V
28 27 a1i ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ V )
29 mpoexga ( ( 𝑈 ∈ WUni ∧ 𝑈 ∈ WUni ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ∈ V )
30 4 4 29 syl2anc ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ∈ V )
31 18 22 rhmresfn ( 𝜑 → ( Hom ‘ 𝑅 ) Fn ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
32 26 28 30 31 resfval2 ( 𝜑 → ( ⟨ ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾f ( Hom ‘ 𝑅 ) ) = ⟨ ( ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) ⟩ )
33 inss1 ( 𝑈 ∩ Ring ) ⊆ 𝑈
34 18 33 eqsstrdi ( 𝜑 → ( Base ‘ 𝑅 ) ⊆ 𝑈 )
35 34 resmptd ( 𝜑 → ( ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) )
36 3 a1i ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
37 36 mpteq1d ( 𝜑 → ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) )
38 5 37 eqtr2d ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) = 𝐹 )
39 35 38 eqtrd ( 𝜑 → ( ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) = 𝐹 )
40 oveq1 ( 𝑥 = 𝑎 → ( 𝑥 RingHom 𝑦 ) = ( 𝑎 RingHom 𝑦 ) )
41 40 reseq2d ( 𝑥 = 𝑎 → ( I ↾ ( 𝑥 RingHom 𝑦 ) ) = ( I ↾ ( 𝑎 RingHom 𝑦 ) ) )
42 oveq2 ( 𝑦 = 𝑏 → ( 𝑎 RingHom 𝑦 ) = ( 𝑎 RingHom 𝑏 ) )
43 42 reseq2d ( 𝑦 = 𝑏 → ( I ↾ ( 𝑎 RingHom 𝑦 ) ) = ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
44 41 43 cbvmpov ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) = ( 𝑎𝐵 , 𝑏𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
45 44 a1i ( 𝜑 → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) = ( 𝑎𝐵 , 𝑏𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) ) )
46 3 a1i ( ( 𝜑𝑎𝐵 ) → 𝐵 = ( Base ‘ 𝑅 ) )
47 eqidd ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
48 fveq2 ( 𝑦 = 𝑏 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑏 ) )
49 fveq2 ( 𝑥 = 𝑎 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑎 ) )
50 48 49 oveqan12rd ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
51 50 reseq2d ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
52 51 adantl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
53 3 34 eqsstrid ( 𝜑𝐵𝑈 )
54 53 sseld ( 𝜑 → ( 𝑎𝐵𝑎𝑈 ) )
55 54 com12 ( 𝑎𝐵 → ( 𝜑𝑎𝑈 ) )
56 55 adantr ( ( 𝑎𝐵𝑏𝐵 ) → ( 𝜑𝑎𝑈 ) )
57 56 impcom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑎𝑈 )
58 53 sseld ( 𝜑 → ( 𝑏𝐵𝑏𝑈 ) )
59 58 adantld ( 𝜑 → ( ( 𝑎𝐵𝑏𝐵 ) → 𝑏𝑈 ) )
60 59 imp ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑏𝑈 )
61 ovexd ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ∈ V )
62 61 resiexd ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ∈ V )
63 47 52 57 60 62 ovmpod ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
64 63 reseq1d ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
65 4 adantr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑈 ∈ WUni )
66 simprl ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑎𝐵 )
67 simprr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑏𝐵 )
68 1 3 65 21 66 67 ringchom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) = ( 𝑎 RingHom 𝑏 ) )
69 68 reseq2d ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RingHom 𝑏 ) ) )
70 eqid ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
71 eqid ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
72 70 71 rhmf ( 𝑓 ∈ ( 𝑎 RingHom 𝑏 ) → 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) )
73 fvex ( Base ‘ 𝑏 ) ∈ V
74 fvex ( Base ‘ 𝑎 ) ∈ V
75 73 74 pm3.2i ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V )
76 75 a1i ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) )
77 elmapg ( ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) → ( 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
78 76 77 syl ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
79 72 78 syl5ibr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑓 ∈ ( 𝑎 RingHom 𝑏 ) → 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
80 79 ssrdv ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 RingHom 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
81 80 resabs1d ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RingHom 𝑏 ) ) = ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
82 64 69 81 3eqtrrd ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( I ↾ ( 𝑎 RingHom 𝑏 ) ) = ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
83 36 46 82 mpoeq123dva ( 𝜑 → ( 𝑎𝐵 , 𝑏𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) ) = ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) )
84 6 45 83 3eqtrrd ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) = 𝐺 )
85 39 84 opeq12d ( 𝜑 → ⟨ ( ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
86 32 85 eqtr2d ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( ⟨ ( 𝑥𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾f ( Hom ‘ 𝑅 ) ) )
87 1 4 18 22 ringcval ( 𝜑𝑅 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) )
88 87 oveq1d ( 𝜑 → ( 𝑅 Func 𝑆 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func 𝑆 ) )
89 24 86 88 3eltr4d ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
90 df-br ( 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
91 89 90 sylibr ( 𝜑𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )