Theorem fldcALTV

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) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		drhmsubcALTV.c	|- C = ( U i^i DivRing )
2		drhmsubcALTV.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
3		fldhmsubcALTV.d	|- D = ( U i^i Field )
4		fldhmsubcALTV.f	|- F = ( r e. D , s e. D |-> ( r RingHom s ) )
5		fvexd	|- ( U e. V -> ( RingCatALTV ` 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 -> ( ( ( RingCatALTV ` U ) |`cat J ) |`cat F ) = ( ( RingCatALTV ` U ) |`cat F ) )
20	1 2 3 4	fldcatALTV	|- ( U e. V -> ( ( RingCatALTV ` U ) |`cat F ) e. Cat )
21	19 20	eqeltrd	|- ( U e. V -> ( ( ( RingCatALTV ` U ) |`cat J ) |`cat F ) e. Cat )