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