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}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}={\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}$$
6	1 3 4 5	ringcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)$$
7	6	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \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){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \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}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)Fn\left(\left(U\cap \mathrm{Ring}\right)\times \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){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)\right)}$$
18	7 8 17	3eqtr4d	$$⊢\phi \to B=U\cap \mathrm{Ring}$$