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 46411
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 46409 . 2 class RngCatALTV
2 vu . . 3 setvar 𝑒
3 cvv 3459 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1540 . . . . 5 class 𝑒
6 crng 46325 . . . . 5 class Rng
75, 6cin 3927 . . . 4 class (𝑒 ∩ Rng)
8 cnx 17091 . . . . . . 7 class ndx
9 cbs 17109 . . . . . . 7 class Base
108, 9cfv 6516 . . . . . 6 class (Baseβ€˜ndx)
114cv 1540 . . . . . 6 class 𝑏
1210, 11cop 4612 . . . . 5 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 chom 17173 . . . . . . 7 class Hom
148, 13cfv 6516 . . . . . 6 class (Hom β€˜ndx)
15 vx . . . . . . 7 setvar π‘₯
16 vy . . . . . . 7 setvar 𝑦
1715cv 1540 . . . . . . . 8 class π‘₯
1816cv 1540 . . . . . . . 8 class 𝑦
19 crngh 46336 . . . . . . . 8 class RngHomo
2017, 18, 19co 7377 . . . . . . 7 class (π‘₯ RngHomo 𝑦)
2115, 16, 11, 11, 20cmpo 7379 . . . . . 6 class (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ RngHomo 𝑦))
2214, 21cop 4612 . . . . 5 class ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ RngHomo 𝑦))⟩
23 cco 17174 . . . . . . 7 class comp
248, 23cfv 6516 . . . . . 6 class (compβ€˜ndx)
25 vv . . . . . . 7 setvar 𝑣
26 vz . . . . . . 7 setvar 𝑧
2711, 11cxp 5651 . . . . . . 7 class (𝑏 Γ— 𝑏)
28 vg . . . . . . . 8 setvar 𝑔
29 vf . . . . . . . 8 setvar 𝑓
3025cv 1540 . . . . . . . . . 10 class 𝑣
31 c2nd 7940 . . . . . . . . . 10 class 2nd
3230, 31cfv 6516 . . . . . . . . 9 class (2nd β€˜π‘£)
3326cv 1540 . . . . . . . . 9 class 𝑧
3432, 33, 19co 7377 . . . . . . . 8 class ((2nd β€˜π‘£) RngHomo 𝑧)
35 c1st 7939 . . . . . . . . . 10 class 1st
3630, 35cfv 6516 . . . . . . . . 9 class (1st β€˜π‘£)
3736, 32, 19co 7377 . . . . . . . 8 class ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£))
3828cv 1540 . . . . . . . . 9 class 𝑔
3929cv 1540 . . . . . . . . 9 class 𝑓
4038, 39ccom 5657 . . . . . . . 8 class (𝑔 ∘ 𝑓)
4128, 29, 34, 37, 40cmpo 7379 . . . . . . 7 class (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓))
4225, 26, 27, 11, 41cmpo 7379 . . . . . 6 class (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓)))
4324, 42cop 4612 . . . . 5 class ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓)))⟩
4412, 22, 43ctp 4610 . . . 4 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ RngHomo 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓)))⟩}
454, 7, 44csb 3873 . . 3 class ⦋(𝑒 ∩ Rng) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ RngHomo 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓)))⟩}
462, 3, 45cmpt 5208 . 2 class (𝑒 ∈ V ↦ ⦋(𝑒 ∩ Rng) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ RngHomo 𝑦))⟩, ⟨(compβ€˜ndx), (𝑣 ∈ (𝑏 Γ— 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘£) RngHomo 𝑧), 𝑓 ∈ ((1st β€˜π‘£) RngHomo (2nd β€˜π‘£)) ↦ (𝑔 ∘ 𝑓)))⟩})
471, 46wceq 1541 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  46412
  Copyright terms: Public domain W3C validator