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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngc	⊢ RngCat
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		cestrc	⊢ ExtStrCat
4	1	cv	⊢ 𝑢
5	4 3	cfv	⊢ ( ExtStrCat ‘ 𝑢 )
6		cresc	⊢ ↾cat
7		crngh	⊢ RngHomo
8		crng	⊢ Rng
9	4 8	cin	⊢ ( 𝑢 ∩ Rng )
10	9 9	cxp	⊢ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) )
11	7 10	cres	⊢ ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) )
12	5 11 6	co	⊢ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) )
13	1 2 12	cmpt	⊢ ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) )
14	0 13	wceq	⊢ RngCat = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHomo ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) )