Metamath Proof Explorer

Theorem fldcatALTV

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

		Ref	Expression
	Hypotheses	drhmsubcALTV.c	$⊢ C = U \cap DivRing$
		drhmsubcALTV.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
		fldhmsubcALTV.d	$⊢ D = U \cap Field$
		fldhmsubcALTV.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
	Assertion	fldcatALTV	$⊢ U \in V \to RingCatALTV (U) ↾_{cat} F \in Cat$

Proof

Step	Hyp	Ref	Expression
1		drhmsubcALTV.c	$⊢ C = U \cap DivRing$
2		drhmsubcALTV.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
3		fldhmsubcALTV.d	$⊢ D = U \cap Field$
4		fldhmsubcALTV.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	sringcatALTV	$⊢ U \in V \to RingCatALTV (U) ↾_{cat} F \in Cat$