Metamath Proof Explorer

Theorem unbnn

Description: Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of Suppes p. 151. See unbnn3 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003)

Ref Expression
Assertion unbnn 
|- ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~~ _om )

Proof

Step Hyp Ref Expression
1 ssdomg 
 |-  ( _om e. _V -> ( A C_ _om -> A ~<_ _om ) )
2 1 imp 
 |-  ( ( _om e. _V /\ A C_ _om ) -> A ~<_ _om )
3 2 3adant3 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~<_ _om )
4 simp1 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> _om e. _V )
5 ssexg 
 |-  ( ( A C_ _om /\ _om e. _V ) -> A e. _V )
6 5 ancoms 
 |-  ( ( _om e. _V /\ A C_ _om ) -> A e. _V )
7 6 3adant3 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A e. _V )
8 eqid 
 |-  ( rec ( ( z e. _V |-> |^| ( A \ suc z ) ) , |^| A ) |` _om ) = ( rec ( ( z e. _V |-> |^| ( A \ suc z ) ) , |^| A ) |` _om )
9 8 unblem4 
 |-  ( ( A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> ( rec ( ( z e. _V |-> |^| ( A \ suc z ) ) , |^| A ) |` _om ) : _om -1-1-> A )
10 9 3adant1 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> ( rec ( ( z e. _V |-> |^| ( A \ suc z ) ) , |^| A ) |` _om ) : _om -1-1-> A )
11 f1dom2g 
 |-  ( ( _om e. _V /\ A e. _V /\ ( rec ( ( z e. _V |-> |^| ( A \ suc z ) ) , |^| A ) |` _om ) : _om -1-1-> A ) -> _om ~<_ A )
12 4 7 10 11 syl3anc 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> _om ~<_ A )
13 sbth 
 |-  ( ( A ~<_ _om /\ _om ~<_ A ) -> A ~~ _om )
14 3 12 13 syl2anc 
 |-  ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~~ _om )