Metamath Proof Explorer

Theorem isinf

Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion isinf 
|- ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( n = (/) -> ( x ~~ n <-> x ~~ (/) ) )
2 1 anbi2d 
 |-  ( n = (/) -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ (/) ) ) )
3 2 exbidv 
 |-  ( n = (/) -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ (/) ) ) )
4 breq2 
 |-  ( n = m -> ( x ~~ n <-> x ~~ m ) )
5 4 anbi2d 
 |-  ( n = m -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ m ) ) )
6 5 exbidv 
 |-  ( n = m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ m ) ) )
7 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
8 7 adantl 
 |-  ( ( n = suc m /\ x = y ) -> ( x C_ A <-> y C_ A ) )
9 breq1 
 |-  ( x = y -> ( x ~~ n <-> y ~~ n ) )
10 breq2 
 |-  ( n = suc m -> ( y ~~ n <-> y ~~ suc m ) )
11 9 10 sylan9bbr 
 |-  ( ( n = suc m /\ x = y ) -> ( x ~~ n <-> y ~~ suc m ) )
12 8 11 anbi12d 
 |-  ( ( n = suc m /\ x = y ) -> ( ( x C_ A /\ x ~~ n ) <-> ( y C_ A /\ y ~~ suc m ) ) )
13 12 cbvexdvaw 
 |-  ( n = suc m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. y ( y C_ A /\ y ~~ suc m ) ) )
14 0ss 
 |-  (/) C_ A
15 0ex 
 |-  (/) e. _V
16 15 enref 
 |-  (/) ~~ (/)
17 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
18 breq1 
 |-  ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) )
19 17 18 anbi12d 
 |-  ( x = (/) -> ( ( x C_ A /\ x ~~ (/) ) <-> ( (/) C_ A /\ (/) ~~ (/) ) ) )
20 15 19 spcev 
 |-  ( ( (/) C_ A /\ (/) ~~ (/) ) -> E. x ( x C_ A /\ x ~~ (/) ) )
21 14 16 20 mp2an 
 |-  E. x ( x C_ A /\ x ~~ (/) )
22 21 a1i 
 |-  ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ (/) ) )
23 ssdif0 
 |-  ( A C_ x <-> ( A \ x ) = (/) )
24 eqss 
 |-  ( x = A <-> ( x C_ A /\ A C_ x ) )
25 breq1 
 |-  ( x = A -> ( x ~~ m <-> A ~~ m ) )
26 25 biimpa 
 |-  ( ( x = A /\ x ~~ m ) -> A ~~ m )
27 rspe 
 |-  ( ( m e. _om /\ A ~~ m ) -> E. m e. _om A ~~ m )
28 26 27 sylan2 
 |-  ( ( m e. _om /\ ( x = A /\ x ~~ m ) ) -> E. m e. _om A ~~ m )
29 isfi 
 |-  ( A e. Fin <-> E. m e. _om A ~~ m )
30 28 29 sylibr 
 |-  ( ( m e. _om /\ ( x = A /\ x ~~ m ) ) -> A e. Fin )
31 30 expcom 
 |-  ( ( x = A /\ x ~~ m ) -> ( m e. _om -> A e. Fin ) )
32 24 31 sylanbr 
 |-  ( ( ( x C_ A /\ A C_ x ) /\ x ~~ m ) -> ( m e. _om -> A e. Fin ) )
33 32 ex 
 |-  ( ( x C_ A /\ A C_ x ) -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) )
34 23 33 sylan2br 
 |-  ( ( x C_ A /\ ( A \ x ) = (/) ) -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) )
35 34 expcom 
 |-  ( ( A \ x ) = (/) -> ( x C_ A -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) ) )
36 35 3impd 
 |-  ( ( A \ x ) = (/) -> ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> A e. Fin ) )
37 36 com12 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( ( A \ x ) = (/) -> A e. Fin ) )
38 37 con3d 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. A e. Fin -> -. ( A \ x ) = (/) ) )
39 bren 
 |-  ( x ~~ m <-> E. f f : x -1-1-onto-> m )
40 neq0 
 |-  ( -. ( A \ x ) = (/) <-> E. z z e. ( A \ x ) )
41 eldifi 
 |-  ( z e. ( A \ x ) -> z e. A )
42 41 snssd 
 |-  ( z e. ( A \ x ) -> { z } C_ A )
43 unss 
 |-  ( ( x C_ A /\ { z } C_ A ) <-> ( x u. { z } ) C_ A )
44 43 biimpi 
 |-  ( ( x C_ A /\ { z } C_ A ) -> ( x u. { z } ) C_ A )
45 42 44 sylan2 
 |-  ( ( x C_ A /\ z e. ( A \ x ) ) -> ( x u. { z } ) C_ A )
46 45 ad2ant2r 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) C_ A )
47 vex 
 |-  z e. _V
48 vex 
 |-  m e. _V
49 47 48 f1osn 
 |-  { <. z , m >. } : { z } -1-1-onto-> { m }
50 49 jctr 
 |-  ( f : x -1-1-onto-> m -> ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) )
51 eldifn 
 |-  ( z e. ( A \ x ) -> -. z e. x )
52 disjsn 
 |-  ( ( x i^i { z } ) = (/) <-> -. z e. x )
53 51 52 sylibr 
 |-  ( z e. ( A \ x ) -> ( x i^i { z } ) = (/) )
54 nnord 
 |-  ( m e. _om -> Ord m )
55 orddisj 
 |-  ( Ord m -> ( m i^i { m } ) = (/) )
56 54 55 syl 
 |-  ( m e. _om -> ( m i^i { m } ) = (/) )
57 53 56 anim12i 
 |-  ( ( z e. ( A \ x ) /\ m e. _om ) -> ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) )
58 f1oun 
 |-  ( ( ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) /\ ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
59 50 57 58 syl2an 
 |-  ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
60 df-suc 
 |-  suc m = ( m u. { m } )
61 f1oeq3 
 |-  ( suc m = ( m u. { m } ) -> ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) ) )
62 60 61 ax-mp 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
63 vex 
 |-  f e. _V
64 snex 
 |-  { <. z , m >. } e. _V
65 63 64 unex 
 |-  ( f u. { <. z , m >. } ) e. _V
66 f1oeq1 
 |-  ( g = ( f u. { <. z , m >. } ) -> ( g : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m ) )
67 65 66 spcev 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
68 bren 
 |-  ( ( x u. { z } ) ~~ suc m <-> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
69 67 68 sylibr 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> ( x u. { z } ) ~~ suc m )
70 62 69 sylbir 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) -> ( x u. { z } ) ~~ suc m )
71 59 70 syl 
 |-  ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) ~~ suc m )
72 71 adantll 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) ~~ suc m )
73 vex 
 |-  x e. _V
74 snex 
 |-  { z } e. _V
75 73 74 unex 
 |-  ( x u. { z } ) e. _V
76 sseq1 
 |-  ( y = ( x u. { z } ) -> ( y C_ A <-> ( x u. { z } ) C_ A ) )
77 breq1 
 |-  ( y = ( x u. { z } ) -> ( y ~~ suc m <-> ( x u. { z } ) ~~ suc m ) )
78 76 77 anbi12d 
 |-  ( y = ( x u. { z } ) -> ( ( y C_ A /\ y ~~ suc m ) <-> ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) ) )
79 75 78 spcev 
 |-  ( ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) -> E. y ( y C_ A /\ y ~~ suc m ) )
80 46 72 79 syl2anc 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> E. y ( y C_ A /\ y ~~ suc m ) )
81 80 expcom 
 |-  ( ( z e. ( A \ x ) /\ m e. _om ) -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
82 81 ex 
 |-  ( z e. ( A \ x ) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
83 82 exlimiv 
 |-  ( E. z z e. ( A \ x ) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
84 40 83 sylbi 
 |-  ( -. ( A \ x ) = (/) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
85 84 com13 
 |-  ( ( x C_ A /\ f : x -1-1-onto-> m ) -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
86 85 expcom 
 |-  ( f : x -1-1-onto-> m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
87 86 exlimiv 
 |-  ( E. f f : x -1-1-onto-> m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
88 39 87 sylbi 
 |-  ( x ~~ m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
89 88 3imp21 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
90 38 89 syld 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) )
91 90 3expia 
 |-  ( ( x C_ A /\ x ~~ m ) -> ( m e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
92 91 exlimiv 
 |-  ( E. x ( x C_ A /\ x ~~ m ) -> ( m e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
93 92 com3l 
 |-  ( m e. _om -> ( -. A e. Fin -> ( E. x ( x C_ A /\ x ~~ m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
94 3 6 13 22 93 finds2 
 |-  ( n e. _om -> ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ n ) ) )
95 94 com12 
 |-  ( -. A e. Fin -> ( n e. _om -> E. x ( x C_ A /\ x ~~ n ) ) )
96 95 ralrimiv 
 |-  ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )