Users' Mathboxes 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 44175
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 44173 . 2 class RingCatALTV
2 vu . . 3 setvar 𝑢
3 cvv 3495 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1527 . . . . 5 class 𝑢
6 crg 19228 . . . . 5 class Ring
75, 6cin 3934 . . . 4 class (𝑢 ∩ Ring)
8 cnx 16470 . . . . . . 7 class ndx
9 cbs 16473 . . . . . . 7 class Base
108, 9cfv 6349 . . . . . 6 class (Base‘ndx)
114cv 1527 . . . . . 6 class 𝑏
1210, 11cop 4565 . . . . 5 class ⟨(Base‘ndx), 𝑏
13 chom 16566 . . . . . . 7 class Hom
148, 13cfv 6349 . . . . . 6 class (Hom ‘ndx)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
1715cv 1527 . . . . . . . 8 class 𝑥
1816cv 1527 . . . . . . . 8 class 𝑦
19 crh 19395 . . . . . . . 8 class RingHom
2017, 18, 19co 7145 . . . . . . 7 class (𝑥 RingHom 𝑦)
2115, 16, 11, 11, 20cmpo 7147 . . . . . 6 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))
2214, 21cop 4565 . . . . 5 class ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩
23 cco 16567 . . . . . . 7 class comp
248, 23cfv 6349 . . . . . 6 class (comp‘ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5547 . . . . . . 7 class (𝑏 × 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1527 . . . . . . . . . 10 class 𝑣
31 c2nd 7679 . . . . . . . . . 10 class 2nd
3230, 31cfv 6349 . . . . . . . . 9 class (2nd𝑣)
3326cv 1527 . . . . . . . . 9 class 𝑧
3432, 33, 19co 7145 . . . . . . . 8 class ((2nd𝑣) RingHom 𝑧)
35 c1st 7678 . . . . . . . . . 10 class 1st
3630, 35cfv 6349 . . . . . . . . 9 class (1st𝑣)
3736, 32, 19co 7145 . . . . . . . 8 class ((1st𝑣) RingHom (2nd𝑣))
3828cv 1527 . . . . . . . . 9 class 𝑔
3929cv 1527 . . . . . . . . 9 class 𝑓
4038, 39ccom 5553 . . . . . . . 8 class (𝑔𝑓)
4128, 29, 34, 37, 40cmpo 7147 . . . . . . 7 class (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))
4225, 26, 27, 11, 41cmpo 7147 . . . . . 6 class (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))
4324, 42cop 4565 . . . . 5 class ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩
4412, 22, 43ctp 4563 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
454, 7, 44csb 3882 . . 3 class (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
462, 3, 45cmpt 5138 . 2 class (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
471, 46wceq 1528 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  44176
  Copyright terms: Public domain W3C validator