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

Definition df-rngcALTV 42285
Description: Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital 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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
Assertion
Ref Expression
df-rngcALTV RngCatALTV = (𝑢 ∈ V ↦ (𝑢 ∩ Rng) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-rngcALTV
StepHypRef Expression
1 crngcALTV 42283 . 2 class RngCatALTV
2 vu . . 3 setvar 𝑢
3 cvv 3231 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1522 . . . . 5 class 𝑢
6 crng 42199 . . . . 5 class Rng
75, 6cin 3606 . . . 4 class (𝑢 ∩ Rng)
8 cnx 15901 . . . . . . 7 class ndx
9 cbs 15904 . . . . . . 7 class Base
108, 9cfv 5926 . . . . . 6 class (Base‘ndx)
114cv 1522 . . . . . 6 class 𝑏
1210, 11cop 4216 . . . . 5 class ⟨(Base‘ndx), 𝑏
13 chom 15999 . . . . . . 7 class Hom
148, 13cfv 5926 . . . . . 6 class (Hom ‘ndx)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
1715cv 1522 . . . . . . . 8 class 𝑥
1816cv 1522 . . . . . . . 8 class 𝑦
19 crngh 42210 . . . . . . . 8 class RngHomo
2017, 18, 19co 6690 . . . . . . 7 class (𝑥 RngHomo 𝑦)
2115, 16, 11, 11, 20cmpt2 6692 . . . . . 6 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))
2214, 21cop 4216 . . . . 5 class ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩
23 cco 16000 . . . . . . 7 class comp
248, 23cfv 5926 . . . . . 6 class (comp‘ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5141 . . . . . . 7 class (𝑏 × 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1522 . . . . . . . . . 10 class 𝑣
31 c2nd 7209 . . . . . . . . . 10 class 2nd
3230, 31cfv 5926 . . . . . . . . 9 class (2nd𝑣)
3326cv 1522 . . . . . . . . 9 class 𝑧
3432, 33, 19co 6690 . . . . . . . 8 class ((2nd𝑣) RngHomo 𝑧)
35 c1st 7208 . . . . . . . . . 10 class 1st
3630, 35cfv 5926 . . . . . . . . 9 class (1st𝑣)
3736, 32, 19co 6690 . . . . . . . 8 class ((1st𝑣) RngHomo (2nd𝑣))
3828cv 1522 . . . . . . . . 9 class 𝑔
3929cv 1522 . . . . . . . . 9 class 𝑓
4038, 39ccom 5147 . . . . . . . 8 class (𝑔𝑓)
4128, 29, 34, 37, 40cmpt2 6692 . . . . . . 7 class (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓))
4225, 26, 27, 11, 41cmpt2 6692 . . . . . 6 class (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))
4324, 42cop 4216 . . . . 5 class ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩
4412, 22, 43ctp 4214 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
454, 7, 44csb 3566 . . 3 class (𝑢 ∩ Rng) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
462, 3, 45cmpt 4762 . 2 class (𝑢 ∈ V ↦ (𝑢 ∩ Rng) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
471, 46wceq 1523 1 wff RngCatALTV = (𝑢 ∈ V ↦ (𝑢 ∩ Rng) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st𝑣) RngHomo (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  rngcvalALTV  42286
  Copyright terms: Public domain W3C validator