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 = ( Base ` R )
	rprmcl.p	|- P = ( RPrime ` R )
	rprmcl.r	|- ( ph -> R e. V )
	rprmcl.x	|- ( ph -> X e. P )
Assertion	rprmcl	|- ( ph -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		rprmcl.b	|- B = ( Base ` R )
2		rprmcl.p	|- P = ( RPrime ` R )
3		rprmcl.r	|- ( ph -> R e. V )
4		rprmcl.x	|- ( ph -> X e. P )
5	4 2	eleqtrdi	|- ( ph -> X e. ( RPrime ` R ) )
6		eqid	|- ( Unit ` R ) = ( Unit ` R )
7		eqid	|- ( 0g ` R ) = ( 0g ` R )
8		eqid	|- ( ||r ` R ) = ( ||r ` R )
9		eqid	|- ( .r ` R ) = ( .r ` R )
10	1 6 7 8 9	isrprm	|- ( R e. V -> ( X e. ( RPrime ` R ) <-> ( X e. ( B \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) /\ A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) ) )
11	10	simprbda	|- ( ( R e. V /\ X e. ( RPrime ` R ) ) -> X e. ( B \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) )
12	11	eldifad	|- ( ( R e. V /\ X e. ( RPrime ` R ) ) -> X e. B )
13	3 5 12	syl2anc	|- ( ph -> X e. B )