Theorem rprmcl

Description: A ring prime is an element of the base set. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmcl.b	$$⊢B={\mathrm{Base}}_R$$
	rprmcl.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmcl.r	$$⊢\phi \to R\in V$$
	rprmcl.x	$$⊢\phi \to X\in P$$
Assertion	rprmcl	$$⊢\phi \to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		rprmcl.b	$$⊢B={\mathrm{Base}}_R$$
2		rprmcl.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		rprmcl.r	$$⊢\phi \to R\in V$$
4		rprmcl.x	$$⊢\phi \to X\in P$$
5	4 2	eleqtrdi	$$⊢\phi \to X\in \mathrm{RPrime}\left(R\right)$$
6		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
7		eqid	$$⊢0_R=0_R$$
8		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
9		eqid	$$⊢{\cdot }_R={\cdot }_R$$
10	1 6 7 8 9	isrprm	$$⊢R\in V\to \left(X\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(X\in \left(B\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{0_R\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(X{\parallel }_r\left(R\right)\left(x{\cdot }_{R}y\right)\to \left(X{\parallel }_r\left(R\right)x\vee X{\parallel }_r\left(R\right)y\right)\right)\right)\right)$$
11	10	simprbda	$$⊢\left(R\in V\wedge X\in \mathrm{RPrime}\left(R\right)\right)\to X\in \left(B\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{0_R\right\}\right)\right)$$
12	11	eldifad	$$⊢\left(R\in V\wedge X\in \mathrm{RPrime}\left(R\right)\right)\to X\in B$$
13	3 5 12	syl2anc	$$⊢\phi \to X\in B$$