# Metamath Proof Explorer

## Theorem ringcbas

Description: Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcbas.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
ringcbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
ringcbas.u ${⊢}{\phi }\to {U}\in {V}$
Assertion ringcbas ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 ringcbas.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
2 ringcbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 ringcbas.u ${⊢}{\phi }\to {U}\in {V}$
4 eqidd ${⊢}{\phi }\to {U}\cap \mathrm{Ring}={U}\cap \mathrm{Ring}$
5 eqidd ${⊢}{\phi }\to {\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}={\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}$
6 1 3 4 5 ringcval ${⊢}{\phi }\to {C}=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)$
7 6 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)\right)}$
8 2 a1i ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
9 eqid ${⊢}\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)$
10 eqid ${⊢}{\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}={\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
11 fvexd ${⊢}{\phi }\to \mathrm{ExtStrCat}\left({U}\right)\in \mathrm{V}$
12 4 5 rhmresfn ${⊢}{\phi }\to \left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)Fn\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)$
13 inss1 ${⊢}{U}\cap \mathrm{Ring}\subseteq {U}$
14 eqid ${⊢}\mathrm{ExtStrCat}\left({U}\right)=\mathrm{ExtStrCat}\left({U}\right)$
15 14 3 estrcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
16 13 15 sseqtrid ${⊢}{\phi }\to {U}\cap \mathrm{Ring}\subseteq {\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
17 9 10 11 12 16 rescbas ${⊢}{\phi }\to {U}\cap \mathrm{Ring}={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)\right)}\right)\right)}$
18 7 8 17 3eqtr4d ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$