Metamath Proof Explorer


Definition df-rngc

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngc
 |-  RngCat
1 vu
 |-  u
2 cvv
 |-  _V
3 cestrc
 |-  ExtStrCat
4 1 cv
 |-  u
5 4 3 cfv
 |-  ( ExtStrCat ` u )
6 cresc
 |-  |`cat
7 crngh
 |-  RngHomo
8 crng
 |-  Rng
9 4 8 cin
 |-  ( u i^i Rng )
10 9 9 cxp
 |-  ( ( u i^i Rng ) X. ( u i^i Rng ) )
11 7 10 cres
 |-  ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) )
12 5 11 6 co
 |-  ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) )
13 1 2 12 cmpt
 |-  ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )
14 0 13 wceq
 |-  RngCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )