Metamath Proof Explorer

Definition df-ringc

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cringc 
 |-  RingCat
1 vu 
 |-  u
2 cvv 
 |-  _V
3 cestrc 
 |-  ExtStrCat
4 1 cv 
 |-  u
5 4 3 cfv 
 |-  ( ExtStrCat ` u )
6 cresc 
 |-  |`cat
7 crh 
 |-  RingHom
8 crg 
 |-  Ring
9 4 8 cin 
 |-  ( u i^i Ring )
10 9 9 cxp 
 |-  ( ( u i^i Ring ) X. ( u i^i Ring ) )
11 7 10 cres 
 |-  ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) )
12 5 11 6 co 
 |-  ( ( ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) )
13 1 2 12 cmpt 
 |-  ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )
14 0 13 wceq 
 |-  RingCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )