Metamath Proof Explorer

Theorem aannen

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

Ref Expression
Assertion aannen 
|- AA ~~ NN

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( a e. NN0 |-> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } ) = ( a e. NN0 |-> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )
2 1 aannenlem3 
 |-  AA ~~ NN