Metamath Proof Explorer

Definition df-rngc

Description: Definition of the category Rng, relativized to a subset u . This is the category of all non-unital rings in u and homomorphisms between these rings. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 27-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Assertion df-rngc ⊢ RngCat = u ∈ V ⟼ ExtStrCat ⁡ u ↾ cat RngHomo ↾ u ∩ Rng × u ∩ Rng

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngc class RngCat
1 vu setvar u
2 cvv class V
3 cestrc class ExtStrCat
4 1 cv setvar u
5 4 3 cfv class ExtStrCat ⁡ u
6 cresc class ↾ cat
7 crngh class RngHomo
8 crng class Rng
9 4 8 cin class u ∩ Rng
10 9 9 cxp class u ∩ Rng × u ∩ Rng
11 7 10 cres class RngHomo ↾ u ∩ Rng × u ∩ Rng
12 5 11 6 co class ExtStrCat ⁡ u ↾ cat RngHomo ↾ u ∩ Rng × u ∩ Rng
13 1 2 12 cmpt class u ∈ V ⟼ ExtStrCat ⁡ u ↾ cat RngHomo ↾ u ∩ Rng × u ∩ Rng
14 0 13 wceq wff RngCat = u ∈ V ⟼ ExtStrCat ⁡ u ↾ cat RngHomo ↾ u ∩ Rng × u ∩ Rng