Theorem aannen

Description: The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Assertion	aannen	⊢ 𝔸 ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } ) = ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } )
2	1	aannenlem3	⊢ 𝔸 ≈ ℕ