Definition df-prm

Description: Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	df-prm	⊢ ℙ = { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprime	⊢ ℙ
1		vp	⊢ 𝑝
2		cn	⊢ ℕ
3		vn	⊢ 𝑛
4	3	cv	⊢ 𝑛
5		cdvds	⊢ ∥
6	1	cv	⊢ 𝑝
7	4 6 5	wbr	⊢ 𝑛 ∥ 𝑝
8	7 3 2	crab	⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 }
9		cen	⊢ ≈
10		c2o	⊢ 2o
11	8 10 9	wbr	⊢ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o
12	11 1 2	crab	⊢ { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }
13	0 12	wceq	⊢ ℙ = { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }