Description: The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | srhmsubcALTV.s | ⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring | |
srhmsubcALTV.c | ⊢ 𝐶 = ( 𝑈 ∩ 𝑆 ) | ||
srhmsubcALTV.j | ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) ) | ||
Assertion | sringcatALTV | ⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srhmsubcALTV.s | ⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring | |
2 | srhmsubcALTV.c | ⊢ 𝐶 = ( 𝑈 ∩ 𝑆 ) | |
3 | srhmsubcALTV.j | ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) ) | |
4 | eqid | ⊢ ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) = ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) | |
5 | 1 2 3 | srhmsubcALTV | ⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCatALTV ‘ 𝑈 ) ) ) |
6 | 4 5 | subccat | ⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat ) |