Theorem rngcbas

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

	Ref	Expression
Hypotheses	rngcbas.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	rngcbas.b	$$⊢B={\mathrm{Base}}_C$$
	rngcbas.u	$$⊢\phi \to U\in V$$
Assertion	rngcbas	$$⊢\phi \to B=U\cap \mathrm{Rng}$$

Proof

Step	Hyp	Ref	Expression
1		rngcbas.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
2		rngcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		rngcbas.u	$$⊢\phi \to U\in V$$
4		eqidd	$$⊢\phi \to U\cap \mathrm{Rng}=U\cap \mathrm{Rng}$$
5		eqidd	$$⊢\phi \to {\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}={\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}$$
6	1 3 4 5	rngcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)$$
7	6	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\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{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\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	rnghmresfn	$$⊢\phi \to \left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)Fn\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)$$
13		inss1	$$⊢U\cap \mathrm{Rng}\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{Rng}\subseteq {\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}$$
17	9 10 11 12 16	rescbas	$$⊢\phi \to U\cap \mathrm{Rng}={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)\right)}$$
18	7 8 17	3eqtr4d	$$⊢\phi \to B=U\cap \mathrm{Rng}$$