Definition df-ringcALTV 42006

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.)

Assertion

Ref	Expression
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 ) ) ) >. } )

Distinct variable group:   f, b, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-ringcALTV

Step	Hyp	Ref	Expression
1		cringcALTV 42004	. 2 class RingCatALTV
2		vu	. . 3 setvar u
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class u
6		crg 18547	. . . . 5 class Ring
7	5, 6	cin 3573	. . . 4 class ( u i^i Ring )
8		cnx 15854	. . . . . . 7 class ndx
9		cbs 15857	. . . . . . 7 class Base
10	8, 9	cfv 5888	. . . . . 6 class ( Base ` ndx )
11	4	cv 1482	. . . . . 6 class b
12	10, 11	cop 4183	. . . . 5 class <. ( Base ` ndx ) , b >.
13		chom 15952	. . . . . . 7 class Hom
14	8, 13	cfv 5888	. . . . . 6 class ( Hom ` ndx )
15		vx	. . . . . . 7 setvar x
16		vy	. . . . . . 7 setvar y
17	15	cv 1482	. . . . . . . 8 class x
18	16	cv 1482	. . . . . . . 8 class y
19		crh 18712	. . . . . . . 8 class RingHom
20	17, 18, 19	co 6650	. . . . . . 7 class ( x RingHom y )
21	15, 16, 11, 11, 20	cmpt2 6652	. . . . . 6 class ( x e. b , y e. b |-> ( x RingHom y ) )
22	14, 21	cop 4183	. . . . 5 class <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RingHom y ) ) >.
23		cco 15953	. . . . . . 7 class comp
24	8, 23	cfv 5888	. . . . . 6 class (comp ` ndx )
25		vv	. . . . . . 7 setvar v
26		vz	. . . . . . 7 setvar z
27	11, 11	cxp 5112	. . . . . . 7 class ( b X. b )
28		vg	. . . . . . . 8 setvar g
29		vf	. . . . . . . 8 setvar f
30	25	cv 1482	. . . . . . . . . 10 class v
31		c2nd 7167	. . . . . . . . . 10 class 2nd
32	30, 31	cfv 5888	. . . . . . . . 9 class ( 2nd ` v )
33	26	cv 1482	. . . . . . . . 9 class z
34	32, 33, 19	co 6650	. . . . . . . 8 class ( ( 2nd ` v ) RingHom z )
35		c1st 7166	. . . . . . . . . 10 class 1st
36	30, 35	cfv 5888	. . . . . . . . 9 class ( 1st ` v )
37	36, 32, 19	co 6650	. . . . . . . 8 class ( ( 1st ` v ) RingHom ( 2nd ` v ) )
38	28	cv 1482	. . . . . . . . 9 class g
39	29	cv 1482	. . . . . . . . 9 class f
40	38, 39	ccom 5118	. . . . . . . 8 class ( g o. f )
41	28, 29, 34, 37, 40	cmpt2 6652	. . . . . . 7 class ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) )
42	25, 26, 27, 11, 41	cmpt2 6652	. . . . . 6 class ( 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	24, 42	cop 4183	. . . . 5 class <. (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	12, 22, 43	ctp 4181	. . . 4 class { <. ( 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	4, 7, 44	csb 3533	. . 3 class [_ ( 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	2, 3, 45	cmpt 4729	. 2 class ( 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 ) ) ) >. } )
47	1, 46	wceq 1483	1 wff 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 ) ) ) >. } )

This definition is referenced by:  ringcvalALTV  42007