This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHom ↾ ( ( 𝑢 ∩ 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 crnghm ⊢ RngHom
8 crng ⊢ Rng
9 4 8 cin ⊢ ( 𝑢 ∩ Rng )
10 9 9 cxp ⊢ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) )
11 7 10 cres ⊢ ( RngHom ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) )
12 5 11 6 co ⊢ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHom ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) )
13 1 2 12 cmpt ⊢ ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHom ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) )
14 0 13 wceq ⊢ RngCat = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RngHom ↾ ( ( 𝑢 ∩ Rng ) × ( 𝑢 ∩ Rng ) ) ) ) )