Metamath Proof Explorer


Theorem drhmsubc

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020)

Ref Expression
Hypotheses drhmsubc.c 𝐶 = ( 𝑈 ∩ DivRing )
drhmsubc.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion drhmsubc ( 𝑈𝑉𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 drhmsubc.c 𝐶 = ( 𝑈 ∩ DivRing )
2 drhmsubc.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3 drngring ( 𝑟 ∈ DivRing → 𝑟 ∈ Ring )
4 3 rgen 𝑟 ∈ DivRing 𝑟 ∈ Ring
5 4 1 2 srhmsubc ( 𝑈𝑉𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )