Metamath Proof Explorer

Theorem fmtnoinf

Description: The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021)

Ref Expression
Assertion fmtnoinf 
|- ran FermatNo e/ Fin

Proof

Step Hyp Ref Expression
1 fmtnof1 
 |-  FermatNo : NN0 -1-1-> NN
2 f1f 
 |-  ( FermatNo : NN0 -1-1-> NN -> FermatNo : NN0 --> NN )
3 fdm 
 |-  ( FermatNo : NN0 --> NN -> dom FermatNo = NN0 )
4 nnssnn0 
 |-  NN C_ NN0
5 nnnfi 
 |-  -. NN e. Fin
6 ssfi 
 |-  ( ( NN0 e. Fin /\ NN C_ NN0 ) -> NN e. Fin )
7 6 expcom 
 |-  ( NN C_ NN0 -> ( NN0 e. Fin -> NN e. Fin ) )
8 7 con3d 
 |-  ( NN C_ NN0 -> ( -. NN e. Fin -> -. NN0 e. Fin ) )
9 4 5 8 mp2 
 |-  -. NN0 e. Fin
10 eleq1 
 |-  ( dom FermatNo = NN0 -> ( dom FermatNo e. Fin <-> NN0 e. Fin ) )
11 9 10 mtbiri 
 |-  ( dom FermatNo = NN0 -> -. dom FermatNo e. Fin )
12 3 11 syl 
 |-  ( FermatNo : NN0 --> NN -> -. dom FermatNo e. Fin )
13 ffun 
 |-  ( FermatNo : NN0 --> NN -> Fun FermatNo )
14 fundmfibi 
 |-  ( Fun FermatNo -> ( FermatNo e. Fin <-> dom FermatNo e. Fin ) )
15 13 14 syl 
 |-  ( FermatNo : NN0 --> NN -> ( FermatNo e. Fin <-> dom FermatNo e. Fin ) )
16 12 15 mtbird 
 |-  ( FermatNo : NN0 --> NN -> -. FermatNo e. Fin )
17 1 2 16 mp2b 
 |-  -. FermatNo e. Fin
18 nn0ex 
 |-  NN0 e. _V
19 f1dmvrnfibi 
 |-  ( ( NN0 e. _V /\ FermatNo : NN0 -1-1-> NN ) -> ( FermatNo e. Fin <-> ran FermatNo e. Fin ) )
20 19 notbid 
 |-  ( ( NN0 e. _V /\ FermatNo : NN0 -1-1-> NN ) -> ( -. FermatNo e. Fin <-> -. ran FermatNo e. Fin ) )
21 18 1 20 mp2an 
 |-  ( -. FermatNo e. Fin <-> -. ran FermatNo e. Fin )
22 17 21 mpbi 
 |-  -. ran FermatNo e. Fin
23 22 nelir 
 |-  ran FermatNo e/ Fin