Definition 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 = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cringc	⊢ RingCat
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		cestrc	⊢ ExtStrCat
4	1	cv	⊢ 𝑢
5	4 3	cfv	⊢ ( ExtStrCat ‘ 𝑢 )
6		cresc	⊢ ↾cat
7		crh	⊢ RingHom
8		crg	⊢ Ring
9	4 8	cin	⊢ ( 𝑢 ∩ Ring )
10	9 9	cxp	⊢ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) )
11	7 10	cres	⊢ ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) )
12	5 11 6	co	⊢ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) )
13	1 2 12	cmpt	⊢ ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) ) )
14	0 13	wceq	⊢ RingCat = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) ) )