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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rprmcl.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	rprmcl.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	rprmcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
Assertion	rprmcl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rprmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rprmcl.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3		rprmcl.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4		rprmcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5	4 2	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( RPrime ‘ 𝑅 ) )
6		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
9		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10	1 6 7 8 9	isrprm	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑋 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑋 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
11	10	simprbda	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ ( RPrime ‘ 𝑅 ) ) → 𝑋 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) )
12	11	eldifad	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ ( RPrime ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
13	3 5 12	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )