Definition df-ringc 42005

Description: Definition of the category Ring, relativized to a subset u. See also the note in [Lang] p. 91, and the item Rng in [Adamek] p. 478. This is the category of all 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, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)

Assertion

Ref	Expression
df-ringc	|- RingCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )

Detailed syntax breakdown of Definition df-ringc

Step	Hyp	Ref	Expression
1		cringc 42003	. 2 class RingCat
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		crh 18712	. . . . 5 class RingHom
8		crg 18547	. . . . . . 7 class Ring
9	4, 8	cin 3573	. . . . . 6 class ( u i^i Ring )
10	9, 9	cxp 5112	. . . . 5 class ( ( u i^i Ring ) X. ( u i^i Ring ) )
11	7, 10	cres 5116	. . . 4 class ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) )
12		cresc 16468	. . . 4 class |`cat
13	6, 11, 12	co 6650	. . 3 class ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) )
14	2, 3, 13	cmpt 4729	. 2 class ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )
15	1, 14	wceq 1483	1 wff RingCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )

This definition is referenced by:  ringcval  42008