Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ringcALTV Structured version   Visualization version   GIF version

Definition df-ringcALTV 44645
 Description: Definition of the category Ring, relativized to a subset 𝑢. This is the category of all rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 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 = (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ringcALTV
StepHypRef Expression
1 cringcALTV 44643 . 2 class RingCatALTV
2 vu . . 3 setvar 𝑢
3 cvv 3441 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1537 . . . . 5 class 𝑢
6 crg 19293 . . . . 5 class Ring
75, 6cin 3880 . . . 4 class (𝑢 ∩ Ring)
8 cnx 16474 . . . . . . 7 class ndx
9 cbs 16477 . . . . . . 7 class Base
108, 9cfv 6324 . . . . . 6 class (Base‘ndx)
114cv 1537 . . . . . 6 class 𝑏
1210, 11cop 4531 . . . . 5 class ⟨(Base‘ndx), 𝑏
13 chom 16570 . . . . . . 7 class Hom
148, 13cfv 6324 . . . . . 6 class (Hom ‘ndx)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
1715cv 1537 . . . . . . . 8 class 𝑥
1816cv 1537 . . . . . . . 8 class 𝑦
19 crh 19463 . . . . . . . 8 class RingHom
2017, 18, 19co 7135 . . . . . . 7 class (𝑥 RingHom 𝑦)
2115, 16, 11, 11, 20cmpo 7137 . . . . . 6 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))
2214, 21cop 4531 . . . . 5 class ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩
23 cco 16571 . . . . . . 7 class comp
248, 23cfv 6324 . . . . . 6 class (comp‘ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5517 . . . . . . 7 class (𝑏 × 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1537 . . . . . . . . . 10 class 𝑣
31 c2nd 7672 . . . . . . . . . 10 class 2nd
3230, 31cfv 6324 . . . . . . . . 9 class (2nd𝑣)
3326cv 1537 . . . . . . . . 9 class 𝑧
3432, 33, 19co 7135 . . . . . . . 8 class ((2nd𝑣) RingHom 𝑧)
35 c1st 7671 . . . . . . . . . 10 class 1st
3630, 35cfv 6324 . . . . . . . . 9 class (1st𝑣)
3736, 32, 19co 7135 . . . . . . . 8 class ((1st𝑣) RingHom (2nd𝑣))
3828cv 1537 . . . . . . . . 9 class 𝑔
3929cv 1537 . . . . . . . . 9 class 𝑓
4038, 39ccom 5523 . . . . . . . 8 class (𝑔𝑓)
4128, 29, 34, 37, 40cmpo 7137 . . . . . . 7 class (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))
4225, 26, 27, 11, 41cmpo 7137 . . . . . 6 class (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))
4324, 42cop 4531 . . . . 5 class ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩
4412, 22, 43ctp 4529 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
454, 7, 44csb 3828 . . 3 class (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
462, 3, 45cmpt 5110 . 2 class (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
471, 46wceq 1538 1 wff RingCatALTV = (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
 Colors of variables: wff setvar class This definition is referenced by:  ringcvalALTV  44646
 Copyright terms: Public domain W3C validator