Metamath Proof Explorer

Theorem aannenlem3

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

Ref Expression
Hypothesis aannenlem.a 
|- H = ( 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 } )
Assertion aannenlem3 
|- AA ~~ NN

Proof

Step Hyp Ref Expression
1 aannenlem.a 
 |-  H = ( 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 aannenlem2 
 |-  AA = U. ran H
3 omelon 
 |-  _om e. On
4 nn0ennn 
 |-  NN0 ~~ NN
5 nnenom 
 |-  NN ~~ _om
6 4 5 entri 
 |-  NN0 ~~ _om
7 6 ensymi 
 |-  _om ~~ NN0
8 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN0 ) -> NN0 e. dom card )
9 3 7 8 mp2an 
 |-  NN0 e. dom card
10 cnex 
 |-  CC e. _V
11 10 rabex 
 |-  { 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 } e. _V
12 11 1 fnmpti 
 |-  H Fn NN0
13 dffn4 
 |-  ( H Fn NN0 <-> H : NN0 -onto-> ran H )
14 12 13 mpbi 
 |-  H : NN0 -onto-> ran H
15 fodomnum 
 |-  ( NN0 e. dom card -> ( H : NN0 -onto-> ran H -> ran H ~<_ NN0 ) )
16 9 14 15 mp2 
 |-  ran H ~<_ NN0
17 domentr 
 |-  ( ( ran H ~<_ NN0 /\ NN0 ~~ _om ) -> ran H ~<_ _om )
18 16 6 17 mp2an 
 |-  ran H ~<_ _om
19 fvelrnb 
 |-  ( H Fn NN0 -> ( f e. ran H <-> E. g e. NN0 ( H ` g ) = f ) )
20 12 19 ax-mp 
 |-  ( f e. ran H <-> E. g e. NN0 ( H ` g ) = f )
21 1 aannenlem1 
 |-  ( g e. NN0 -> ( H ` g ) e. Fin )
22 eleq1 
 |-  ( ( H ` g ) = f -> ( ( H ` g ) e. Fin <-> f e. Fin ) )
23 21 22 syl5ibcom 
 |-  ( g e. NN0 -> ( ( H ` g ) = f -> f e. Fin ) )
24 23 rexlimiv 
 |-  ( E. g e. NN0 ( H ` g ) = f -> f e. Fin )
25 20 24 sylbi 
 |-  ( f e. ran H -> f e. Fin )
26 25 ssriv 
 |-  ran H C_ Fin
27 aasscn 
 |-  AA C_ CC
28 2 27 eqsstrri 
 |-  U. ran H C_ CC
29 soss 
 |-  ( U. ran H C_ CC -> ( f Or CC -> f Or U. ran H ) )
30 28 29 ax-mp 
 |-  ( f Or CC -> f Or U. ran H )
31 iunfictbso 
 |-  ( ( ran H ~<_ _om /\ ran H C_ Fin /\ f Or U. ran H ) -> U. ran H ~<_ _om )
32 18 26 30 31 mp3an12i 
 |-  ( f Or CC -> U. ran H ~<_ _om )
33 2 32 eqbrtrid 
 |-  ( f Or CC -> AA ~<_ _om )
34 cnso 
 |-  E. f f Or CC
35 33 34 exlimiiv 
 |-  AA ~<_ _om
36 5 ensymi 
 |-  _om ~~ NN
37 domentr 
 |-  ( ( AA ~<_ _om /\ _om ~~ NN ) -> AA ~<_ NN )
38 35 36 37 mp2an 
 |-  AA ~<_ NN
39 10 27 ssexi 
 |-  AA e. _V
40 nnssq 
 |-  NN C_ QQ
41 qssaa 
 |-  QQ C_ AA
42 40 41 sstri 
 |-  NN C_ AA
43 ssdomg 
 |-  ( AA e. _V -> ( NN C_ AA -> NN ~<_ AA ) )
44 39 42 43 mp2 
 |-  NN ~<_ AA
45 sbth 
 |-  ( ( AA ~<_ NN /\ NN ~<_ AA ) -> AA ~~ NN )
46 38 44 45 mp2an 
 |-  AA ~~ NN