Theorem ufdprmidl

Description: In a unique factorization domain R , a nonzero prime ideal J contains a prime element p . (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	isufd.i	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
	isufd.3	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	isufd.0	⊢ 0 = ( 0g ‘ 𝑅 )
	ufdprmidl.2	⊢ ( 𝜑 → 𝑅 ∈ UFD )
	ufdprmidl.3	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
	ufdprmidl.4	⊢ ( 𝜑 → 𝐽 ≠ { 0 } )
Assertion	ufdprmidl	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		isufd.i	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
2		isufd.3	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3		isufd.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		ufdprmidl.2	⊢ ( 𝜑 → 𝑅 ∈ UFD )
5		ufdprmidl.3	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
6		ufdprmidl.4	⊢ ( 𝜑 → 𝐽 ≠ { 0 } )
7		ineq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∩ 𝑃 ) = ( 𝐽 ∩ 𝑃 ) )
8	7	neeq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ∩ 𝑃 ) ≠ ∅ ↔ ( 𝐽 ∩ 𝑃 ) ≠ ∅ ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( 𝑗 ∩ 𝑃 ) ≠ ∅ ↔ ( 𝐽 ∩ 𝑃 ) ≠ ∅ ) )
10		incom	⊢ ( 𝑃 ∩ 𝐽 ) = ( 𝐽 ∩ 𝑃 )
11	10	neeq1i	⊢ ( ( 𝑃 ∩ 𝐽 ) ≠ ∅ ↔ ( 𝐽 ∩ 𝑃 ) ≠ ∅ )
12		inn0	⊢ ( ( 𝑃 ∩ 𝐽 ) ≠ ∅ ↔ ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝐽 )
13	11 12	bitr3i	⊢ ( ( 𝐽 ∩ 𝑃 ) ≠ ∅ ↔ ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝐽 )
14	9 13	bitrdi	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( 𝑗 ∩ 𝑃 ) ≠ ∅ ↔ ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝐽 ) )
15	5 6	eldifsnd	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐼 ∖ { { 0 } } ) )
16	1 2 3	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑗 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ ) )
17	16	simprbi	⊢ ( 𝑅 ∈ UFD → ∀ 𝑗 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ )
18	4 17	syl	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ )
19	14 15 18	rspcdv2	⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝐽 )