Theorem crhmsubcALTV

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 commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	crhmsubcALTV.c	⊢ 𝐶 = ( 𝑈 ∩ CRing )
	crhmsubcALTV.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	crhmsubcALTV	⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCatALTV ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		crhmsubcALTV.c	⊢ 𝐶 = ( 𝑈 ∩ CRing )
2		crhmsubcALTV.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3		crngring	⊢ ( 𝑟 ∈ CRing → 𝑟 ∈ Ring )
4	3	rgen	⊢ ∀ 𝑟 ∈ CRing 𝑟 ∈ Ring
5	4 1 2	srhmsubcALTV	⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCatALTV ‘ 𝑈 ) ) )