MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isinf Structured version   Unicode version

Theorem isinf 7787
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 has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.)
Assertion
Ref Expression
isinf  |-  ( -.  A  e.  Fin  ->  A. n  e.  om  E. x ( x  C_  A  /\  x  ~~  n
) )
Distinct variable group:    x, A, n

Proof of Theorem isinf
Dummy variables  f  m  y  z  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4424 . . . . . 6  |-  ( n  =  (/)  ->  ( x 
~~  n  <->  x  ~~  (/) ) )
21anbi2d 708 . . . . 5  |-  ( n  =  (/)  ->  ( ( x  C_  A  /\  x  ~~  n )  <->  ( x  C_  A  /\  x  ~~  (/) ) ) )
32exbidv 1758 . . . 4  |-  ( n  =  (/)  ->  ( E. x ( x  C_  A  /\  x  ~~  n
)  <->  E. x ( x 
C_  A  /\  x  ~~  (/) ) ) )
4 breq2 4424 . . . . . 6  |-  ( n  =  m  ->  (
x  ~~  n  <->  x  ~~  m ) )
54anbi2d 708 . . . . 5  |-  ( n  =  m  ->  (
( x  C_  A  /\  x  ~~  n )  <-> 
( x  C_  A  /\  x  ~~  m ) ) )
65exbidv 1758 . . . 4  |-  ( n  =  m  ->  ( E. x ( x  C_  A  /\  x  ~~  n
)  <->  E. x ( x 
C_  A  /\  x  ~~  m ) ) )
7 sseq1 3485 . . . . . . 7  |-  ( x  =  y  ->  (
x  C_  A  <->  y  C_  A ) )
87adantl 467 . . . . . 6  |-  ( ( n  =  suc  m  /\  x  =  y
)  ->  ( x  C_  A  <->  y  C_  A
) )
9 breq1 4423 . . . . . . 7  |-  ( x  =  y  ->  (
x  ~~  n  <->  y  ~~  n ) )
10 breq2 4424 . . . . . . 7  |-  ( n  =  suc  m  -> 
( y  ~~  n  <->  y 
~~  suc  m )
)
119, 10sylan9bbr 705 . . . . . 6  |-  ( ( n  =  suc  m  /\  x  =  y
)  ->  ( x  ~~  n  <->  y  ~~  suc  m ) )
128, 11anbi12d 715 . . . . 5  |-  ( ( n  =  suc  m  /\  x  =  y
)  ->  ( (
x  C_  A  /\  x  ~~  n )  <->  ( y  C_  A  /\  y  ~~  suc  m ) ) )
1312cbvexdva 2086 . . . 4  |-  ( n  =  suc  m  -> 
( E. x ( x  C_  A  /\  x  ~~  n )  <->  E. y
( y  C_  A  /\  y  ~~  suc  m
) ) )
14 0ss 3791 . . . . . 6  |-  (/)  C_  A
15 0ex 4552 . . . . . . 7  |-  (/)  e.  _V
1615enref 7605 . . . . . 6  |-  (/)  ~~  (/)
17 sseq1 3485 . . . . . . . 8  |-  ( x  =  (/)  ->  ( x 
C_  A  <->  (/)  C_  A
) )
18 breq1 4423 . . . . . . . 8  |-  ( x  =  (/)  ->  ( x 
~~  (/)  <->  (/)  ~~  (/) ) )
1917, 18anbi12d 715 . . . . . . 7  |-  ( x  =  (/)  ->  ( ( x  C_  A  /\  x  ~~  (/) )  <->  ( (/)  C_  A  /\  (/)  ~~  (/) ) ) )
2015, 19spcev 3173 . . . . . 6  |-  ( (
(/)  C_  A  /\  (/)  ~~  (/) )  ->  E. x ( x  C_  A  /\  x  ~~  (/) ) )
2114, 16, 20mp2an 676 . . . . 5  |-  E. x
( x  C_  A  /\  x  ~~  (/) )
2221a1i 11 . . . 4  |-  ( -.  A  e.  Fin  ->  E. x ( x  C_  A  /\  x  ~~  (/) ) )
23 ssdif0 3851 . . . . . . . . . . . . 13  |-  ( A 
C_  x  <->  ( A  \  x )  =  (/) )
24 eqss 3479 . . . . . . . . . . . . . . 15  |-  ( x  =  A  <->  ( x  C_  A  /\  A  C_  x ) )
25 breq1 4423 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  A  ->  (
x  ~~  m  <->  A  ~~  m ) )
2625biimpa 486 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  A  /\  x  ~~  m )  ->  A  ~~  m )
27 rspe 2883 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  om  /\  A  ~~  m )  ->  E. m  e.  om  A  ~~  m )
2826, 27sylan2 476 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  om  /\  ( x  =  A  /\  x  ~~  m ) )  ->  E. m  e.  om  A  ~~  m
)
29 isfi 7596 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  Fin  <->  E. m  e.  om  A  ~~  m
)
3028, 29sylibr 215 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  om  /\  ( x  =  A  /\  x  ~~  m ) )  ->  A  e.  Fin )
3130expcom 436 . . . . . . . . . . . . . . 15  |-  ( ( x  =  A  /\  x  ~~  m )  -> 
( m  e.  om  ->  A  e.  Fin )
)
3224, 31sylanbr 475 . . . . . . . . . . . . . 14  |-  ( ( ( x  C_  A  /\  A  C_  x )  /\  x  ~~  m
)  ->  ( m  e.  om  ->  A  e.  Fin ) )
3332ex 435 . . . . . . . . . . . . 13  |-  ( ( x  C_  A  /\  A  C_  x )  -> 
( x  ~~  m  ->  ( m  e.  om  ->  A  e.  Fin )
) )
3423, 33sylan2br 478 . . . . . . . . . . . 12  |-  ( ( x  C_  A  /\  ( A  \  x
)  =  (/) )  -> 
( x  ~~  m  ->  ( m  e.  om  ->  A  e.  Fin )
) )
3534expcom 436 . . . . . . . . . . 11  |-  ( ( A  \  x )  =  (/)  ->  ( x 
C_  A  ->  (
x  ~~  m  ->  ( m  e.  om  ->  A  e.  Fin ) ) ) )
36353impd 1219 . . . . . . . . . 10  |-  ( ( A  \  x )  =  (/)  ->  ( ( x  C_  A  /\  x  ~~  m  /\  m  e.  om )  ->  A  e.  Fin ) )
3736com12 32 . . . . . . . . 9  |-  ( ( x  C_  A  /\  x  ~~  m  /\  m  e.  om )  ->  (
( A  \  x
)  =  (/)  ->  A  e.  Fin ) )
3837con3d 138 . . . . . . . 8  |-  ( ( x  C_  A  /\  x  ~~  m  /\  m  e.  om )  ->  ( -.  A  e.  Fin  ->  -.  ( A  \  x )  =  (/) ) )
39 bren 7582 . . . . . . . . . . 11  |-  ( x 
~~  m  <->  E. f 
f : x -1-1-onto-> m )
40 neq0 3772 . . . . . . . . . . . . . . 15  |-  ( -.  ( A  \  x
)  =  (/)  <->  E. z 
z  e.  ( A 
\  x ) )
41 eldifi 3587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ( A  \  x )  ->  z  e.  A )
4241snssd 4142 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( A  \  x )  ->  { z }  C_  A )
43 unss 3640 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  C_  A  /\  { z }  C_  A
)  <->  ( x  u. 
{ z } ) 
C_  A )
4443biimpi 197 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  C_  A  /\  { z }  C_  A
)  ->  ( x  u.  { z } ) 
C_  A )
4542, 44sylan2 476 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  C_  A  /\  z  e.  ( A  \  x ) )  -> 
( x  u.  {
z } )  C_  A )
4645ad2ant2r 751 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  C_  A  /\  f : x -1-1-onto-> m )  /\  ( z  e.  ( A  \  x
)  /\  m  e.  om ) )  ->  (
x  u.  { z } )  C_  A
)
47 vex 3084 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  z  e. 
_V
48 vex 3084 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  m  e. 
_V
4947, 48f1osn 5864 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { <. z ,  m >. } : { z } -1-1-onto-> { m }
5049jctr 544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : x -1-1-onto-> m  ->  ( f : x -1-1-onto-> m  /\  { <. z ,  m >. } : { z } -1-1-onto-> { m } ) )
51 eldifn 3588 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  ( A  \  x )  ->  -.  z  e.  x )
52 disjsn 4057 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  i^i  { z } )  =  (/)  <->  -.  z  e.  x )
5351, 52sylibr 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( A  \  x )  ->  (
x  i^i  { z } )  =  (/) )
54 nnord 6710 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  om  ->  Ord  m )
55 orddisj 5476 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Ord  m  ->  ( m  i^i  { m } )  =  (/) )
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  om  ->  (
m  i^i  { m } )  =  (/) )
5753, 56anim12i 568 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  e.  ( A 
\  x )  /\  m  e.  om )  ->  ( ( x  i^i 
{ z } )  =  (/)  /\  (
m  i^i  { m } )  =  (/) ) )
58 f1oun 5846 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 } ) )
5950, 57, 58syl2an 479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 5444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  suc  m  =  ( m  u. 
{ m } )
61 f1oeq3 5820 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } ) ) )
6260, 61ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 3084 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  f  e. 
_V
64 snex 4658 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { <. z ,  m >. }  e.  _V
6563, 64unex 6599 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  u.  { <. z ,  m >. } )  e. 
_V
66 f1oeq1 5818 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) )
6765, 66spcev 3173 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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 7582 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  u.  { z } )  ~~  suc  m 
<->  E. g  g : ( x  u.  {
z } ) -1-1-onto-> suc  m
)
6967, 68sylibr 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  u.  { <. z ,  m >. } ) : ( x  u. 
{ z } ) -1-1-onto-> suc  m  ->  ( x  u.  { z } ) 
~~  suc  m )
7062, 69sylbir 216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  u.  { <. z ,  m >. } ) : ( x  u. 
{ z } ) -1-1-onto-> ( m  u.  { m } )  ->  (
x  u.  { z } )  ~~  suc  m )
7159, 70syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f : x -1-1-onto-> m  /\  ( z  e.  ( A  \  x )  /\  m  e.  om ) )  ->  (
x  u.  { z } )  ~~  suc  m )
7271adantll 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  C_  A  /\  f : x -1-1-onto-> m )  /\  ( z  e.  ( A  \  x
)  /\  m  e.  om ) )  ->  (
x  u.  { z } )  ~~  suc  m )
73 vex 3084 . . . . . . . . . . . . . . . . . . . . 21  |-  x  e. 
_V
74 snex 4658 . . . . . . . . . . . . . . . . . . . . 21  |-  { z }  e.  _V
7573, 74unex 6599 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  u.  { z } )  e.  _V
76 sseq1 3485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  u. 
{ z } )  ->  ( y  C_  A 
<->  ( x  u.  {
z } )  C_  A ) )
77 breq1 4423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  u. 
{ z } )  ->  ( y  ~~  suc  m  <->  ( x  u. 
{ z } ) 
~~  suc  m )
)
7876, 77anbi12d 715 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( x  u. 
{ z } )  ->  ( ( y 
C_  A  /\  y  ~~  suc  m )  <->  ( (
x  u.  { z } )  C_  A  /\  ( x  u.  {
z } )  ~~  suc  m ) ) )
7975, 78spcev 3173 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  u.  {
z } )  C_  A  /\  ( x  u. 
{ z } ) 
~~  suc  m )  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) )
8046, 72, 79syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  C_  A  /\  f : x -1-1-onto-> m )  /\  ( z  e.  ( A  \  x
)  /\  m  e.  om ) )  ->  E. y
( y  C_  A  /\  y  ~~  suc  m
) )
8180expcom 436 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  ( A 
\  x )  /\  m  e.  om )  ->  ( ( x  C_  A  /\  f : x -1-1-onto-> m )  ->  E. y
( y  C_  A  /\  y  ~~  suc  m
) ) )
8281ex 435 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( A  \  x )  ->  (
m  e.  om  ->  ( ( x  C_  A  /\  f : x -1-1-onto-> m )  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) )
8382exlimiv 1766 . . . . . . . . . . . . . . 15  |-  ( 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
) ) ) )
8440, 83sylbi 198 . . . . . . . . . . . . . 14  |-  ( -.  ( A  \  x
)  =  (/)  ->  (
m  e.  om  ->  ( ( x  C_  A  /\  f : x -1-1-onto-> m )  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) )
8584com13 83 . . . . . . . . . . . . 13  |-  ( ( x  C_  A  /\  f : x -1-1-onto-> m )  ->  (
m  e.  om  ->  ( -.  ( A  \  x )  =  (/)  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) )
8685expcom 436 . . . . . . . . . . . 12  |-  ( f : x -1-1-onto-> m  ->  ( x 
C_  A  ->  (
m  e.  om  ->  ( -.  ( A  \  x )  =  (/)  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) ) )
8786exlimiv 1766 . . . . . . . . . . 11  |-  ( E. f  f : x -1-1-onto-> m  ->  ( x  C_  A  ->  ( m  e. 
om  ->  ( -.  ( A  \  x )  =  (/)  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) ) )
8839, 87sylbi 198 . . . . . . . . . 10  |-  ( x 
~~  m  ->  (
x  C_  A  ->  ( m  e.  om  ->  ( -.  ( A  \  x )  =  (/)  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) ) )
8988com12 32 . . . . . . . . 9  |-  ( x 
C_  A  ->  (
x  ~~  m  ->  ( m  e.  om  ->  ( -.  ( A  \  x )  =  (/)  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) ) )
90893imp 1199 . . . . . . . 8  |-  ( ( x  C_  A  /\  x  ~~  m  /\  m  e.  om )  ->  ( -.  ( A  \  x
)  =  (/)  ->  E. y
( y  C_  A  /\  y  ~~  suc  m
) ) )
9138, 90syld 45 . . . . . . 7  |-  ( ( x  C_  A  /\  x  ~~  m  /\  m  e.  om )  ->  ( -.  A  e.  Fin  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) )
92913expia 1207 . . . . . 6  |-  ( ( x  C_  A  /\  x  ~~  m )  -> 
( m  e.  om  ->  ( -.  A  e. 
Fin  ->  E. y ( y 
C_  A  /\  y  ~~  suc  m ) ) ) )
9392exlimiv 1766 . . . . 5  |-  ( E. x ( x  C_  A  /\  x  ~~  m
)  ->  ( m  e.  om  ->  ( -.  A  e.  Fin  ->  E. y
( y  C_  A  /\  y  ~~  suc  m
) ) ) )
9493com3l 84 . . . 4  |-  ( m  e.  om  ->  ( -.  A  e.  Fin  ->  ( E. x ( x  C_  A  /\  x  ~~  m )  ->  E. y ( y  C_  A  /\  y  ~~  suc  m ) ) ) )
953, 6, 13, 22, 94finds2 6731 . . 3  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  E. x ( x 
C_  A  /\  x  ~~  n ) ) )
9695com12 32 . 2  |-  ( -.  A  e.  Fin  ->  ( n  e.  om  ->  E. x ( x  C_  A  /\  x  ~~  n
) ) )
9796ralrimiv 2837 1  |-  ( -.  A  e.  Fin  ->  A. n  e.  om  E. x ( x  C_  A  /\  x  ~~  n
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1868   A.wral 2775   E.wrex 2776    \ cdif 3433    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761   {csn 3996   <.cop 4002   class class class wbr 4420   Ord word 5437   suc csuc 5440   -1-1-onto->wf1o 5596   omcom 6702    ~~ cen 7570   Fincfn 7573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-om 6703  df-en 7574  df-fin 7577
This theorem is referenced by:  fineqvlem  7788  isinffi  8427  domtriomlem  8872  ishashinf  12623
  Copyright terms: Public domain W3C validator