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 \cap DivRing$
		drhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
		fldhmsubc.d	$⊢ D = U \cap Field$
		fldhmsubc.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
	Assertion	fldcat	$⊢ U \in V \to RingCat (U) ↾_{cat} F \in Cat$

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	$⊢ C = U \cap DivRing$
2		drhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
3		fldhmsubc.d	$⊢ D = U \cap Field$
4		fldhmsubc.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
5		isfld	$⊢ r \in Field \leftrightarrow (r \in DivRing \land r \in CRing)$
6		crngring	$⊢ r \in CRing \to r \in Ring$
7	6	adantl	$⊢ (r \in DivRing \land r \in CRing) \to r \in Ring$
8	5 7	sylbi	$⊢ r \in Field \to r \in Ring$
9	8	rgen	$⊢ \forall r \in Field r \in Ring$
10	9 3 4	sringcat	$⊢ U \in V \to RingCat (U) ↾_{cat} F \in Cat$