Definition df-rngc 41959

Description: Definition of the category Rng, relativized to a subset u. This is the category of all non-unital rings in u and homomorphisms between these rings. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)

Assertion

Ref	Expression
df-rngc	|- RngCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )

Detailed syntax breakdown of Definition df-rngc

Step	Hyp	Ref	Expression
1		crngc 41957	. 2 class RngCat
2		vu	. . 3 setvar u
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class u
5		cestrc 16762	. . . . 5 class ExtStrCat
6	4, 5	cfv 5888	. . . 4 class (ExtStrCat ` u )
7		crngh 41885	. . . . 5 class RngHomo
8		crng 41874	. . . . . . 7 class Rng
9	4, 8	cin 3573	. . . . . 6 class ( u i^i Rng )
10	9, 9	cxp 5112	. . . . 5 class ( ( u i^i Rng ) X. ( u i^i Rng ) )
11	7, 10	cres 5116	. . . 4 class ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) )
12		cresc 16468	. . . 4 class |`cat
13	6, 11, 12	co 6650	. . 3 class ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) )
14	2, 3, 13	cmpt 4729	. 2 class ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )
15	1, 14	wceq 1483	1 wff RngCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )

This definition is referenced by:  rngcval  41962