Metamath Proof Explorer

Definition df-rngcALTV

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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Assertion df-rngcALTV 
|- RngCatALTV = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngcALTV 
 |-  RngCatALTV
1 vu 
 |-  u
2 cvv 
 |-  _V
3 1 cv 
 |-  u
4 crng 
 |-  Rng
5 3 4 cin 
 |-  ( u i^i Rng )
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 crngh 
 |-  RngHomo
18 15 cv 
 |-  y
19 16 18 17 co 
 |-  ( x RngHomo y )
20 14 15 10 10 19 cmpo 
 |-  ( x e. b , y e. b |-> ( x RngHomo y ) )
21 13 20 cop 
 |-  <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo 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 ) RngHomo z )
33 vf 
 |-  f
34 c1st 
 |-  1st
35 29 34 cfv 
 |-  ( 1st ` v )
36 35 30 17 co 
 |-  ( ( 1st ` v ) RngHomo ( 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 ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) )
41 24 26 25 10 40 cmpo 
 |-  ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) )
42 23 41 cop 
 |-  <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >.
43 11 21 42 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. }
44 6 5 43 csb 
 |-  [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. }
45 1 2 44 cmpt 
 |-  ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
46 0 45 wceq 
 |-  RngCatALTV = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )