Theorem rngcrescrhm

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Hypotheses	rngcrescrhm.u	|- ( ph -> U e. V )
	rngcrescrhm.c	|- C = ( RngCat ` U )
	rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
	rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
Assertion	rngcrescrhm	|- ( ph -> ( C |`cat H ) = ( ( C |`s R ) sSet <. ( Hom ` ndx ) , H >. ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	|- ( ph -> U e. V )
2		rngcrescrhm.c	|- C = ( RngCat ` U )
3		rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
4		rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
5		eqid	|- ( C |`cat H ) = ( C |`cat H )
6	2	fvexi	|- C e. _V
7	6	a1i	|- ( ph -> C e. _V )
8		incom	|- ( Ring i^i U ) = ( U i^i Ring )
9	3 8	eqtrdi	|- ( ph -> R = ( U i^i Ring ) )
10		inex1g	|- ( U e. V -> ( U i^i Ring ) e. _V )
11	1 10	syl	|- ( ph -> ( U i^i Ring ) e. _V )
12	9 11	eqeltrd	|- ( ph -> R e. _V )
13		inss1	|- ( Ring i^i U ) C_ Ring
14	3 13	eqsstrdi	|- ( ph -> R C_ Ring )
15		xpss12	|- ( ( R C_ Ring /\ R C_ Ring ) -> ( R X. R ) C_ ( Ring X. Ring ) )
16	14 14 15	syl2anc	|- ( ph -> ( R X. R ) C_ ( Ring X. Ring ) )
17		rhmfn	|- RingHom Fn ( Ring X. Ring )
18		fnssresb	|- ( RingHom Fn ( Ring X. Ring ) -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
19	17 18	mp1i	|- ( ph -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
20	16 19	mpbird	|- ( ph -> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
21	4	fneq1i	|- ( H Fn ( R X. R ) <-> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
22	20 21	sylibr	|- ( ph -> H Fn ( R X. R ) )
23	5 7 12 22	rescval2	|- ( ph -> ( C |`cat H ) = ( ( C |`s R ) sSet <. ( Hom ` ndx ) , H >. ) )