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 41771
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 41769 . 2 class RingCatALTV
2 vu . . 3 setvar 𝑢
3 cvv 3195 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1480 . . . . 5 class 𝑢
6 crg 18528 . . . . 5 class Ring
75, 6cin 3566 . . . 4 class (𝑢 ∩ Ring)
8 cnx 15835 . . . . . . 7 class ndx
9 cbs 15838 . . . . . . 7 class Base
108, 9cfv 5876 . . . . . 6 class (Base‘ndx)
114cv 1480 . . . . . 6 class 𝑏
1210, 11cop 4174 . . . . 5 class ⟨(Base‘ndx), 𝑏
13 chom 15933 . . . . . . 7 class Hom
148, 13cfv 5876 . . . . . 6 class (Hom ‘ndx)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
1715cv 1480 . . . . . . . 8 class 𝑥
1816cv 1480 . . . . . . . 8 class 𝑦
19 crh 18693 . . . . . . . 8 class RingHom
2017, 18, 19co 6635 . . . . . . 7 class (𝑥 RingHom 𝑦)
2115, 16, 11, 11, 20cmpt2 6637 . . . . . 6 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))
2214, 21cop 4174 . . . . 5 class ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩
23 cco 15934 . . . . . . 7 class comp
248, 23cfv 5876 . . . . . 6 class (comp‘ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5102 . . . . . . 7 class (𝑏 × 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1480 . . . . . . . . . 10 class 𝑣
31 c2nd 7152 . . . . . . . . . 10 class 2nd
3230, 31cfv 5876 . . . . . . . . 9 class (2nd𝑣)
3326cv 1480 . . . . . . . . 9 class 𝑧
3432, 33, 19co 6635 . . . . . . . 8 class ((2nd𝑣) RingHom 𝑧)
35 c1st 7151 . . . . . . . . . 10 class 1st
3630, 35cfv 5876 . . . . . . . . 9 class (1st𝑣)
3736, 32, 19co 6635 . . . . . . . 8 class ((1st𝑣) RingHom (2nd𝑣))
3828cv 1480 . . . . . . . . 9 class 𝑔
3929cv 1480 . . . . . . . . 9 class 𝑓
4038, 39ccom 5108 . . . . . . . 8 class (𝑔𝑓)
4128, 29, 34, 37, 40cmpt2 6637 . . . . . . 7 class (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))
4225, 26, 27, 11, 41cmpt2 6637 . . . . . 6 class (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))
4324, 42cop 4174 . . . . 5 class ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩
4412, 22, 43ctp 4172 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
454, 7, 44csb 3526 . . 3 class (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}
462, 3, 45cmpt 4720 . 2 class (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
471, 46wceq 1481 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  41772
  Copyright terms: Public domain W3C validator