Metamath Proof Explorer

Theorem infpssr

Description: Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion infpssr 
|- ( ( X C. A /\ X ~~ A ) -> _om ~<_ A )

Proof

Step Hyp Ref Expression
1 pssnel 
 |-  ( X C. A -> E. y ( y e. A /\ -. y e. X ) )
2 1 adantr 
 |-  ( ( X C. A /\ X ~~ A ) -> E. y ( y e. A /\ -. y e. X ) )
3 eldif 
 |-  ( y e. ( A \ X ) <-> ( y e. A /\ -. y e. X ) )
4 pssss 
 |-  ( X C. A -> X C_ A )
5 bren 
 |-  ( X ~~ A <-> E. f f : X -1-1-onto-> A )
6 simpr 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> f : X -1-1-onto-> A )
7 f1ofo 
 |-  ( f : X -1-1-onto-> A -> f : X -onto-> A )
8 forn 
 |-  ( f : X -onto-> A -> ran f = A )
9 6 7 8 3syl 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> ran f = A )
10 vex 
 |-  f e. _V
11 10 rnex 
 |-  ran f e. _V
12 9 11 eqeltrrdi 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> A e. _V )
13 simplr 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> X C_ A )
14 simpll 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> y e. ( A \ X ) )
15 eqid 
 |-  ( rec ( `' f , y ) |` _om ) = ( rec ( `' f , y ) |` _om )
16 13 6 14 15 infpssrlem5 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> ( A e. _V -> _om ~<_ A ) )
17 12 16 mpd 
 |-  ( ( ( y e. ( A \ X ) /\ X C_ A ) /\ f : X -1-1-onto-> A ) -> _om ~<_ A )
18 17 ex 
 |-  ( ( y e. ( A \ X ) /\ X C_ A ) -> ( f : X -1-1-onto-> A -> _om ~<_ A ) )
19 18 exlimdv 
 |-  ( ( y e. ( A \ X ) /\ X C_ A ) -> ( E. f f : X -1-1-onto-> A -> _om ~<_ A ) )
20 5 19 biimtrid 
 |-  ( ( y e. ( A \ X ) /\ X C_ A ) -> ( X ~~ A -> _om ~<_ A ) )
21 20 ex 
 |-  ( y e. ( A \ X ) -> ( X C_ A -> ( X ~~ A -> _om ~<_ A ) ) )
22 4 21 syl5 
 |-  ( y e. ( A \ X ) -> ( X C. A -> ( X ~~ A -> _om ~<_ A ) ) )
23 22 impd 
 |-  ( y e. ( A \ X ) -> ( ( X C. A /\ X ~~ A ) -> _om ~<_ A ) )
24 3 23 sylbir 
 |-  ( ( y e. A /\ -. y e. X ) -> ( ( X C. A /\ X ~~ A ) -> _om ~<_ A ) )
25 24 exlimiv 
 |-  ( E. y ( y e. A /\ -. y e. X ) -> ( ( X C. A /\ X ~~ A ) -> _om ~<_ A ) )
26 2 25 mpcom 
 |-  ( ( X C. A /\ X ~~ A ) -> _om ~<_ A )