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 e. _V |-> [_ ( u i^i Ring ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )

Detailed syntax breakdown

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