Theorem fldc

Description: The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	drhmsubc.c	|- C = ( U i^i DivRing )
	drhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
	fldhmsubc.d	|- D = ( U i^i Field )
	fldhmsubc.f	|- F = ( r e. D , s e. D |-> ( r RingHom s ) )
Assertion	fldc	|- ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) e. Cat )

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	|- C = ( U i^i DivRing )
2		drhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
3		fldhmsubc.d	|- D = ( U i^i Field )
4		fldhmsubc.f	|- F = ( r e. D , s e. D |-> ( r RingHom s ) )
5		fvexd	|- ( U e. V -> ( RingCat ` U ) e. _V )
6		ovex	|- ( r RingHom s ) e. _V
7	2 6	fnmpoi	|- J Fn ( C X. C )
8	7	a1i	|- ( U e. V -> J Fn ( C X. C ) )
9	4 6	fnmpoi	|- F Fn ( D X. D )
10	9	a1i	|- ( U e. V -> F Fn ( D X. D ) )
11		inex1g	|- ( U e. V -> ( U i^i DivRing ) e. _V )
12	1 11	eqeltrid	|- ( U e. V -> C e. _V )
13		df-field	|- Field = ( DivRing i^i CRing )
14		inss1	|- ( DivRing i^i CRing ) C_ DivRing
15	13 14	eqsstri	|- Field C_ DivRing
16		sslin	|- ( Field C_ DivRing -> ( U i^i Field ) C_ ( U i^i DivRing ) )
17	15 16	mp1i	|- ( U e. V -> ( U i^i Field ) C_ ( U i^i DivRing ) )
18	17 3 1	3sstr4g	|- ( U e. V -> D C_ C )
19	5 8 10 12 18	rescabs	|- ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) = ( ( RingCat ` U ) |`cat F ) )
20	1 2 3 4	fldcat	|- ( U e. V -> ( ( RingCat ` U ) |`cat F ) e. Cat )
21	19 20	eqeltrd	|- ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) e. Cat )