Definition df-ufd

Description: Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025)

	Ref	Expression
Assertion	df-ufd	⊢ UFD = { 𝑟 ∈ IDomn ∣ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufd	⊢ UFD
1		vr	⊢ 𝑟
2		cidom	⊢ IDomn
3		vi	⊢ 𝑖
4		cprmidl	⊢ PrmIdeal
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( PrmIdeal ‘ 𝑟 )
7		c0g	⊢ 0g
8	5 7	cfv	⊢ ( 0g ‘ 𝑟 )
9	8	csn	⊢ { ( 0g ‘ 𝑟 ) }
10	9	csn	⊢ { { ( 0g ‘ 𝑟 ) } }
11	6 10	cdif	⊢ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } )
12	3	cv	⊢ 𝑖
13		crpm	⊢ RPrime
14	5 13	cfv	⊢ ( RPrime ‘ 𝑟 )
15	12 14	cin	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) )
16		c0	⊢ ∅
17	15 16	wne	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
18	17 3 11	wral	⊢ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
19	18 1 2	crab	⊢ { 𝑟 ∈ IDomn ∣ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ }
20	0 19	wceq	⊢ UFD = { 𝑟 ∈ IDomn ∣ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ }