Definition df-ufd 33554

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.)

Assertion

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

Distinct variable group:   𝑖,𝑟

Detailed syntax breakdown of Definition df-ufd

Step	Hyp	Ref	Expression
1		cufd 33553	. 2 class UFD
2		vi	. . . . . . 7 setvar 𝑖
3	2	cv 1539	. . . . . 6 class 𝑖
4		vr	. . . . . . . 8 setvar 𝑟
5	4	cv 1539	. . . . . . 7 class 𝑟
6		crpm 20424	. . . . . . 7 class RPrime
7	5, 6	cfv 6559	. . . . . 6 class (RPrime‘𝑟)
8	3, 7	cin 3949	. . . . 5 class (𝑖 ∩ (RPrime‘𝑟))
9		c0 4332	. . . . 5 class ∅
10	8, 9	wne 2939	. . . 4 wff (𝑖 ∩ (RPrime‘𝑟)) ≠ ∅
11		cprmidl 33450	. . . . . 6 class PrmIdeal
12	5, 11	cfv 6559	. . . . 5 class (PrmIdeal‘𝑟)
13		c0g 17480	. . . . . . . 8 class 0g
14	5, 13	cfv 6559	. . . . . . 7 class (0g‘𝑟)
15	14	csn 4624	. . . . . 6 class {(0g‘𝑟)}
16	15	csn 4624	. . . . 5 class {{(0g‘𝑟)}}
17	12, 16	cdif 3947	. . . 4 class ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})
18	10, 2, 17	wral 3060	. . 3 wff ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅
19		cidom 20685	. . 3 class IDomn
20	18, 4, 19	crab 3435	. 2 class {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅}
21	1, 20	wceq 1540	1 wff UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅}

This definition is referenced by:  isufd  33555