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 \in V ⟼ ExtStrCat (u) ↾_{cat} ({RngHom ↾}_{((u \cap Rng) \times (u \cap 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		crnghm	$class RngHom$
8		crng	$class Rng$
9	4 8	cin	$class (u \cap Rng)$
10	9 9	cxp	$class ((u \cap Rng) \times (u \cap Rng))$
11	7 10	cres	$class ({RngHom ↾}_{((u \cap Rng) \times (u \cap Rng))})$
12	5 11 6	co	$class (ExtStrCat (u) ↾_{cat} ({RngHom ↾}_{((u \cap Rng) \times (u \cap Rng))}))$
13	1 2 12	cmpt	$class (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RngHom ↾}_{((u \cap Rng) \times (u \cap Rng))}))$
14	0 13	wceq	$wff RngCat = (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RngHom ↾}_{((u \cap Rng) \times (u \cap Rng))}))$

Metamath Proof Explorer

Definition df-rngc

Detailed syntax breakdown