ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  phpm Unicode version

Theorem phpm 6637
Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. By "proper subset" here we mean that there is an element which is in the natural number and not in the subset, or in symbols  E. x x  e.  ( A  \  B
) (which is stronger than not being equal in the absence of excluded middle). Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 6624 through phplem4 6627, nneneq 6629, and this final piece of the proof. (Contributed by NM, 29-May-1998.)
Assertion
Ref Expression
phpm  |-  ( ( A  e.  om  /\  B  C_  A  /\  E. x  x  e.  ( A  \  B ) )  ->  -.  A  ~~  B )
Distinct variable groups:    x, A    x, B

Proof of Theorem phpm
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 simpr 109 . . . . . 6  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  A  =  (/) )  ->  A  =  (/) )
2 eldifi 3125 . . . . . . . . 9  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
3 ne0i 3295 . . . . . . . . 9  |-  ( x  e.  A  ->  A  =/=  (/) )
42, 3syl 14 . . . . . . . 8  |-  ( x  e.  ( A  \  B )  ->  A  =/=  (/) )
54neneqd 2277 . . . . . . 7  |-  ( x  e.  ( A  \  B )  ->  -.  A  =  (/) )
65ad2antlr 474 . . . . . 6  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  A  =  (/) )  ->  -.  A  =  (/) )
71, 6pm2.21dd 586 . . . . 5  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  A  =  (/) )  ->  -.  A  ~~  B )
8 php5dom 6635 . . . . . . . . . 10  |-  ( y  e.  om  ->  -.  suc  y  ~<_  y )
98ad2antlr 474 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  -.  suc  y  ~<_  y )
10 simplr 498 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  /\  y  e.  om )  /\  A  =  suc  y )  /\  A  ~~  B )  ->  A  =  suc  y )
11 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  /\  y  e.  om )  /\  A  =  suc  y )  /\  A  ~~  B )  ->  A  ~~  B )
12 vex 2625 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
1312sucex 4331 . . . . . . . . . . . . . . 15  |-  suc  y  e.  _V
14 difss 3129 . . . . . . . . . . . . . . 15  |-  ( suc  y  \  { x } )  C_  suc  y
1513, 14ssexi 3985 . . . . . . . . . . . . . 14  |-  ( suc  y  \  { x } )  e.  _V
16 eldifn 3126 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A  \  B )  ->  -.  x  e.  B )
1716ad3antlr 478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  -.  x  e.  B
)
18 simpllr 502 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  y  e. 
om )  ->  B  C_  A )
1918adantr 271 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  B  C_  A )
20 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  A  =  suc  y )
2119, 20sseqtrd 3065 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  B  C_  suc  y )
22 ssdif 3138 . . . . . . . . . . . . . . . 16  |-  ( B 
C_  suc  y  ->  ( B  \  { x } )  C_  ( suc  y  \  { x } ) )
23 disjsn 3510 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  i^i  { x } )  =  (/)  <->  -.  x  e.  B )
24 disj3 3341 . . . . . . . . . . . . . . . . . 18  |-  ( ( B  i^i  { x } )  =  (/)  <->  B  =  ( B  \  { x } ) )
2523, 24bitr3i 185 . . . . . . . . . . . . . . . . 17  |-  ( -.  x  e.  B  <->  B  =  ( B  \  { x } ) )
26 sseq1 3050 . . . . . . . . . . . . . . . . 17  |-  ( B  =  ( B  \  { x } )  ->  ( B  C_  ( suc  y  \  {
x } )  <->  ( B  \  { x } ) 
C_  ( suc  y  \  { x } ) ) )
2725, 26sylbi 120 . . . . . . . . . . . . . . . 16  |-  ( -.  x  e.  B  -> 
( B  C_  ( suc  y  \  { x } )  <->  ( B  \  { x } ) 
C_  ( suc  y  \  { x } ) ) )
2822, 27syl5ibr 155 . . . . . . . . . . . . . . 15  |-  ( -.  x  e.  B  -> 
( B  C_  suc  y  ->  B  C_  ( suc  y  \  { x } ) ) )
2917, 21, 28sylc 62 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  B  C_  ( suc  y  \  { x } ) )
30 ssdomg 6551 . . . . . . . . . . . . . 14  |-  ( ( suc  y  \  {
x } )  e. 
_V  ->  ( B  C_  ( suc  y  \  {
x } )  ->  B  ~<_  ( suc  y  \  { x } ) ) )
3115, 29, 30mpsyl 65 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  B  ~<_  ( suc  y  \  { x } ) )
32 simplr 498 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  -> 
y  e.  om )
332ad3antlr 478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  x  e.  A )
3433, 20eleqtrd 2167 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  x  e.  suc  y )
35 phplem3g 6628 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  om  /\  x  e.  suc  y )  ->  y  ~~  ( suc  y  \  { x } ) )
3635ensymd 6556 . . . . . . . . . . . . . 14  |-  ( ( y  e.  om  /\  x  e.  suc  y )  ->  ( suc  y  \  { x } ) 
~~  y )
3732, 34, 36syl2anc 404 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  -> 
( suc  y  \  { x } ) 
~~  y )
38 domentr 6564 . . . . . . . . . . . . 13  |-  ( ( B  ~<_  ( suc  y  \  { x } )  /\  ( suc  y  \  { x } ) 
~~  y )  ->  B  ~<_  y )
3931, 37, 38syl2anc 404 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  B  ~<_  y )
4039adantr 271 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  /\  y  e.  om )  /\  A  =  suc  y )  /\  A  ~~  B )  ->  B  ~<_  y )
41 endomtr 6563 . . . . . . . . . . 11  |-  ( ( A  ~~  B  /\  B  ~<_  y )  ->  A  ~<_  y )
4211, 40, 41syl2anc 404 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  /\  y  e.  om )  /\  A  =  suc  y )  /\  A  ~~  B )  ->  A  ~<_  y )
4310, 42eqbrtrrd 3875 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  /\  y  e.  om )  /\  A  =  suc  y )  /\  A  ~~  B )  ->  suc  y  ~<_  y )
449, 43mtand 627 . . . . . . . 8  |-  ( ( ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B
) )  /\  y  e.  om )  /\  A  =  suc  y )  ->  -.  A  ~~  B )
4544ex 114 . . . . . . 7  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  y  e. 
om )  ->  ( A  =  suc  y  ->  -.  A  ~~  B ) )
4645rexlimdva 2491 . . . . . 6  |-  ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  ->  ( E. y  e.  om  A  =  suc  y  ->  -.  A  ~~  B ) )
4746imp 123 . . . . 5  |-  ( ( ( ( A  e. 
om  /\  B  C_  A
)  /\  x  e.  ( A  \  B ) )  /\  E. y  e.  om  A  =  suc  y )  ->  -.  A  ~~  B )
48 nn0suc 4434 . . . . . 6  |-  ( A  e.  om  ->  ( A  =  (/)  \/  E. y  e.  om  A  =  suc  y ) )
4948ad2antrr 473 . . . . 5  |-  ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  ->  ( A  =  (/)  \/  E. y  e. 
om  A  =  suc  y ) )
507, 47, 49mpjaodan 748 . . . 4  |-  ( ( ( A  e.  om  /\  B  C_  A )  /\  x  e.  ( A  \  B ) )  ->  -.  A  ~~  B )
5150ex 114 . . 3  |-  ( ( A  e.  om  /\  B  C_  A )  -> 
( x  e.  ( A  \  B )  ->  -.  A  ~~  B ) )
5251exlimdv 1748 . 2  |-  ( ( A  e.  om  /\  B  C_  A )  -> 
( E. x  x  e.  ( A  \  B )  ->  -.  A  ~~  B ) )
53523impia 1141 1  |-  ( ( A  e.  om  /\  B  C_  A  /\  E. x  x  e.  ( A  \  B ) )  ->  -.  A  ~~  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 665    /\ w3a 925    = wceq 1290   E.wex 1427    e. wcel 1439    =/= wne 2256   E.wrex 2361   _Vcvv 2622    \ cdif 2999    i^i cin 3001    C_ wss 3002   (/)c0 3289   {csn 3452   class class class wbr 3853   suc csuc 4203   omcom 4420    ~~ cen 6511    ~<_ cdom 6512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-iinf 4418
This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-br 3854  df-opab 3908  df-tr 3945  df-id 4131  df-iord 4204  df-on 4206  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-er 6308  df-en 6514  df-dom 6515
This theorem is referenced by:  phpelm  6638
  Copyright terms: Public domain W3C validator