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	|- I = ( PrmIdeal ` R )
	isufd.3	|- P = ( RPrime ` R )
	isufd.0	|- .0. = ( 0g ` R )
	ufdprmidl.2	|- ( ph -> R e. UFD )
	ufdprmidl.3	|- ( ph -> J e. I )
	ufdprmidl.4	|- ( ph -> J =/= { .0. } )
Assertion	ufdprmidl	|- ( ph -> E. p e. P p e. J )

Proof

Step	Hyp	Ref	Expression
1		isufd.i	|- I = ( PrmIdeal ` R )
2		isufd.3	|- P = ( RPrime ` R )
3		isufd.0	|- .0. = ( 0g ` R )
4		ufdprmidl.2	|- ( ph -> R e. UFD )
5		ufdprmidl.3	|- ( ph -> J e. I )
6		ufdprmidl.4	|- ( ph -> J =/= { .0. } )
7		ineq1	|- ( j = J -> ( j i^i P ) = ( J i^i P ) )
8	7	neeq1d	|- ( j = J -> ( ( j i^i P ) =/= (/) <-> ( J i^i P ) =/= (/) ) )
9	8	adantl	|- ( ( ph /\ j = J ) -> ( ( j i^i P ) =/= (/) <-> ( J i^i P ) =/= (/) ) )
10		incom	|- ( P i^i J ) = ( J i^i P )
11	10	neeq1i	|- ( ( P i^i J ) =/= (/) <-> ( J i^i P ) =/= (/) )
12		inn0	|- ( ( P i^i J ) =/= (/) <-> E. p e. P p e. J )
13	11 12	bitr3i	|- ( ( J i^i P ) =/= (/) <-> E. p e. P p e. J )
14	9 13	bitrdi	|- ( ( ph /\ j = J ) -> ( ( j i^i P ) =/= (/) <-> E. p e. P p e. J ) )
15	5 6	eldifsnd	|- ( ph -> J e. ( I \ { { .0. } } ) )
16	1 2 3	isufd	|- ( R e. UFD <-> ( R e. IDomn /\ A. j e. ( I \ { { .0. } } ) ( j i^i P ) =/= (/) ) )
17	16	simprbi	|- ( R e. UFD -> A. j e. ( I \ { { .0. } } ) ( j i^i P ) =/= (/) )
18	4 17	syl	|- ( ph -> A. j e. ( I \ { { .0. } } ) ( j i^i P ) =/= (/) )
19	14 15 18	rspcdv2	|- ( ph -> E. p e. P p e. J )