Metamath Proof Explorer

Theorem fisdomnn

Description: A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025)

Ref Expression
Assertion fisdomnn 
|- ( A e. Fin -> A ~< NN )

Proof

Step Hyp Ref Expression
1 canth2g 
 |-  ( A e. Fin -> A ~< ~P A )
2 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
3 fzfi 
 |-  ( 1 ... ( # ` ~P A ) ) e. Fin
4 nnex 
 |-  NN e. _V
5 fz1ssnn 
 |-  ( 1 ... ( # ` ~P A ) ) C_ NN
6 ssdomfi2 
 |-  ( ( ( 1 ... ( # ` ~P A ) ) e. Fin /\ NN e. _V /\ ( 1 ... ( # ` ~P A ) ) C_ NN ) -> ( 1 ... ( # ` ~P A ) ) ~<_ NN )
7 3 4 5 6 mp3an 
 |-  ( 1 ... ( # ` ~P A ) ) ~<_ NN
8 isfinite4 
 |-  ( ~P A e. Fin <-> ( 1 ... ( # ` ~P A ) ) ~~ ~P A )
9 domen1 
 |-  ( ( 1 ... ( # ` ~P A ) ) ~~ ~P A -> ( ( 1 ... ( # ` ~P A ) ) ~<_ NN <-> ~P A ~<_ NN ) )
10 8 9 sylbi 
 |-  ( ~P A e. Fin -> ( ( 1 ... ( # ` ~P A ) ) ~<_ NN <-> ~P A ~<_ NN ) )
11 7 10 mpbii 
 |-  ( ~P A e. Fin -> ~P A ~<_ NN )
12 2 11 sylbi 
 |-  ( A e. Fin -> ~P A ~<_ NN )
13 sdomdomtrfi 
 |-  ( ( A e. Fin /\ A ~< ~P A /\ ~P A ~<_ NN ) -> A ~< NN )
14 1 12 13 mpd3an23 
 |-  ( A e. Fin -> A ~< NN )