Metamath Proof Explorer


Definition df-ringcALTV

Description: Definition of the category Ring, relativized to a subset u . This is the category of all 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) (New usage is discouraged.)

Ref Expression
Assertion df-ringcALTV RingCatALTV = u V u Ring / b Base ndx b Hom ndx x b , y b x RingHom y comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cringcALTV class RingCatALTV
1 vu setvar u
2 cvv class V
3 1 cv setvar u
4 crg class Ring
5 3 4 cin class u Ring
6 vb setvar b
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 6 cv setvar b
11 9 10 cop class Base ndx b
12 chom class Hom
13 8 12 cfv class Hom ndx
14 vx setvar x
15 vy setvar y
16 14 cv setvar x
17 crh class RingHom
18 15 cv setvar y
19 16 18 17 co class x RingHom y
20 14 15 10 10 19 cmpo class x b , y b x RingHom y
21 13 20 cop class Hom ndx x b , y b x RingHom y
22 cco class comp
23 8 22 cfv class comp ndx
24 vv setvar v
25 10 10 cxp class b × b
26 vz setvar z
27 vg setvar g
28 c2nd class 2 nd
29 24 cv setvar v
30 29 28 cfv class 2 nd v
31 26 cv setvar z
32 30 31 17 co class 2 nd v RingHom z
33 vf setvar f
34 c1st class 1 st
35 29 34 cfv class 1 st v
36 35 30 17 co class 1 st v RingHom 2 nd v
37 27 cv setvar g
38 33 cv setvar f
39 37 38 ccom class g f
40 27 33 32 36 39 cmpo class g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
41 24 26 25 10 40 cmpo class v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
42 23 41 cop class comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
43 11 21 42 ctp class Base ndx b Hom ndx x b , y b x RingHom y comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
44 6 5 43 csb class u Ring / b Base ndx b Hom ndx x b , y b x RingHom y comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
45 1 2 44 cmpt class u V u Ring / b Base ndx b Hom ndx x b , y b x RingHom y comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f
46 0 45 wceq wff RingCatALTV = u V u Ring / b Base ndx b Hom ndx x b , y b x RingHom y comp ndx v b × b , z b g 2 nd v RingHom z , f 1 st v RingHom 2 nd v g f