Metamath Proof Explorer

Theorem ringcbasbas

Description: An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020)

		Ref	Expression
	Hypotheses	ringcbasbas.r	$⊢ C = RingCat (U)$
		ringcbasbas.b	$⊢ B = {Base}_{C}$
		ringcbasbas.u	$⊢ φ \to U \in WUni$
	Assertion	ringcbasbas	$⊢ (φ \land R \in B) \to {Base}_{R} \in U$

Proof

Step	Hyp	Ref	Expression
1		ringcbasbas.r	$⊢ C = RingCat (U)$
2		ringcbasbas.b	$⊢ B = {Base}_{C}$
3		ringcbasbas.u	$⊢ φ \to U \in WUni$
4	1 2 3	ringcbas	$⊢ φ \to B = U \cap Ring$
5	4	eleq2d	$⊢ φ \to (R \in B \leftrightarrow R \in (U \cap Ring))$
6		elin	$⊢ R \in (U \cap Ring) \leftrightarrow (R \in U \land R \in Ring)$
7		df-base	$⊢ Base = Slot 1$
8		simpl	$⊢ (U \in WUni \land R \in U) \to U \in WUni$
9		simpr	$⊢ (U \in WUni \land R \in U) \to R \in U$
10	7 8 9	wunstr	$⊢ (U \in WUni \land R \in U) \to {Base}_{R} \in U$
11	10	ex	$⊢ U \in WUni \to (R \in U \to {Base}_{R} \in U)$
12	11 3	syl11	$⊢ R \in U \to (φ \to {Base}_{R} \in U)$
13	12	adantr	$⊢ (R \in U \land R \in Ring) \to (φ \to {Base}_{R} \in U)$
14	6 13	sylbi	$⊢ R \in (U \cap Ring) \to (φ \to {Base}_{R} \in U)$
15	14	com12	$⊢ φ \to (R \in (U \cap Ring) \to {Base}_{R} \in U)$
16	5 15	sylbid	$⊢ φ \to (R \in B \to {Base}_{R} \in U)$
17	16	imp	$⊢ (φ \land R \in B) \to {Base}_{R} \in U$