df-ringc

Description: Definition of the category Ring, relativized to a subset u . See also the note in Lang p. 91, and the item Rng in Adamek p. 478. This is the category of all 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, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

		Ref	Expression
	Assertion	df-ringc	$⊢ RingCat = (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cringc	$class RingCat$
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		crh	$class RingHom$
8		crg	$class Ring$
9	4 8	cin	$class (u \cap Ring)$
10	9 9	cxp	$class ((u \cap Ring) \times (u \cap Ring))$
11	7 10	cres	$class ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))})$
12	5 11 6	co	$class (ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}))$
13	1 2 12	cmpt	$class (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}))$
14	0 13	wceq	$wff RingCat = (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}))$

Metamath Proof Explorer

Definition df-ringc

Detailed syntax breakdown