Definition df-rngcALTV 45406

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

Step	Hyp	Ref	Expression
1		crngcALTV 45404	. 2 class RngCatALTV
2		vu	. . 3 setvar 𝑢
3		cvv 3422	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . 5 class 𝑢
6		crng 45320	. . . . 5 class Rng
7	5, 6	cin 3882	. . . 4 class (𝑢 ∩ Rng)
8		cnx 16822	. . . . . . 7 class ndx
9		cbs 16840	. . . . . . 7 class Base
10	8, 9	cfv 6418	. . . . . 6 class (Base‘ndx)
11	4	cv 1538	. . . . . 6 class 𝑏
12	10, 11	cop 4564	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
13		chom 16899	. . . . . . 7 class Hom
14	8, 13	cfv 6418	. . . . . 6 class (Hom ‘ndx)
15		vx	. . . . . . 7 setvar 𝑥
16		vy	. . . . . . 7 setvar 𝑦
17	15	cv 1538	. . . . . . . 8 class 𝑥
18	16	cv 1538	. . . . . . . 8 class 𝑦
19		crngh 45331	. . . . . . . 8 class RngHomo
20	17, 18, 19	co 7255	. . . . . . 7 class (𝑥 RngHomo 𝑦)
21	15, 16, 11, 11, 20	cmpo 7257	. . . . . 6 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))
22	14, 21	cop 4564	. . . . 5 class ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩
23		cco 16900	. . . . . . 7 class comp
24	8, 23	cfv 6418	. . . . . 6 class (comp‘ndx)
25		vv	. . . . . . 7 setvar 𝑣
26		vz	. . . . . . 7 setvar 𝑧
27	11, 11	cxp 5578	. . . . . . 7 class (𝑏 × 𝑏)
28		vg	. . . . . . . 8 setvar 𝑔
29		vf	. . . . . . . 8 setvar 𝑓
30	25	cv 1538	. . . . . . . . . 10 class 𝑣
31		c2nd 7803	. . . . . . . . . 10 class 2nd
32	30, 31	cfv 6418	. . . . . . . . 9 class (2nd ‘𝑣)
33	26	cv 1538	. . . . . . . . 9 class 𝑧
34	32, 33, 19	co 7255	. . . . . . . 8 class ((2nd ‘𝑣) RngHomo 𝑧)
35		c1st 7802	. . . . . . . . . 10 class 1st
36	30, 35	cfv 6418	. . . . . . . . 9 class (1st ‘𝑣)
37	36, 32, 19	co 7255	. . . . . . . 8 class ((1st ‘𝑣) RngHomo (2nd ‘𝑣))
38	28	cv 1538	. . . . . . . . 9 class 𝑔
39	29	cv 1538	. . . . . . . . 9 class 𝑓
40	38, 39	ccom 5584	. . . . . . . 8 class (𝑔 ∘ 𝑓)
41	28, 29, 34, 37, 40	cmpo 7257	. . . . . . 7 class (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓))
42	25, 26, 27, 11, 41	cmpo 7257	. . . . . 6 class (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))
43	24, 42	cop 4564	. . . . 5 class ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩
44	12, 22, 43	ctp 4562	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩}
45	4, 7, 44	csb 3828	. . 3 class ⦋(𝑢 ∩ Rng) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩}
46	2, 3, 45	cmpt 5153	. 2 class (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
47	1, 46	wceq 1539	1 wff RngCatALTV = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})

This definition is referenced by:  rngcvalALTV  45407