Metamath Proof Explorer


Theorem fldcat

Description: The restriction of the category of (unital) 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 fldcat
|- ( U e. V -> ( ( RingCat ` U ) |`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 isfld
 |-  ( r e. Field <-> ( r e. DivRing /\ r e. CRing ) )
6 crngring
 |-  ( r e. CRing -> r e. Ring )
7 6 adantl
 |-  ( ( r e. DivRing /\ r e. CRing ) -> r e. Ring )
8 5 7 sylbi
 |-  ( r e. Field -> r e. Ring )
9 8 rgen
 |-  A. r e. Field r e. Ring
10 9 3 4 sringcat
 |-  ( U e. V -> ( ( RingCat ` U ) |`cat F ) e. Cat )