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 \in V ⟼ ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ 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 \cap 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 \in b, y \in b ⟼ x RingHom y)$
21	13 20	cop	$class ⟨Hom (ndx), (x \in b, y \in 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 \times 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 \circ f)$
40	27 33 32 36 39	cmpo	$class (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)$
41	24 26 25 10 40	cmpo	$class (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
42	23 41	cop	$class ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩$
43	11 21 42	ctp	$class \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\}$
44	6 5 43	csb	$class ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\}$
45	1 2 44	cmpt	$class (u \in V ⟼ ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
46	0 45	wceq	$wff RingCatALTV = (u \in V ⟼ ⦋ (u \cap Ring) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$

Metamath Proof Explorer

Definition df-ringcALTV

Detailed syntax breakdown