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

Theorem php3 7755
Description: Corollary of Pigeonhole Principle. If  A is finite and  B is a proper subset of  A, the  B is strictly less numerous than  A. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
php3  |-  ( ( A  e.  Fin  /\  B  C.  A )  ->  B  ~<  A )

Proof of Theorem php3
Dummy variables  x  f  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 7590 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 relen 7571 . . . . . . . . 9  |-  Rel  ~~
32brrelexi 4874 . . . . . . . 8  |-  ( A 
~~  x  ->  A  e.  _V )
4 pssss 3527 . . . . . . . 8  |-  ( B 
C.  A  ->  B  C_  A )
5 ssdomg 7612 . . . . . . . . 9  |-  ( A  e.  _V  ->  ( B  C_  A  ->  B  ~<_  A ) )
65imp 431 . . . . . . . 8  |-  ( ( A  e.  _V  /\  B  C_  A )  ->  B  ~<_  A )
73, 4, 6syl2an 480 . . . . . . 7  |-  ( ( A  ~~  x  /\  B  C.  A )  ->  B  ~<_  A )
87adantll 719 . . . . . 6  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  B  ~<_  A )
9 bren 7575 . . . . . . . . 9  |-  ( A 
~~  x  <->  E. f 
f : A -1-1-onto-> x )
10 imass2 5203 . . . . . . . . . . . . . . . . 17  |-  ( B 
C_  A  ->  (
f " B ) 
C_  ( f " A ) )
114, 10syl 17 . . . . . . . . . . . . . . . 16  |-  ( B 
C.  A  ->  (
f " B ) 
C_  ( f " A ) )
1211adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C_  ( f " A ) )
13 pssnel 3831 . . . . . . . . . . . . . . . . 17  |-  ( B 
C.  A  ->  E. y
( y  e.  A  /\  -.  y  e.  B
) )
14 eldif 3413 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( A  \  B )  <->  ( y  e.  A  /\  -.  y  e.  B ) )
15 f1ofn 5813 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : A -1-1-onto-> x  ->  f  Fn  A )
16 difss 3559 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A 
\  B )  C_  A
17 fnfvima 6141 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  Fn  A  /\  ( A  \  B ) 
C_  A  /\  y  e.  ( A  \  B
) )  ->  (
f `  y )  e.  ( f " ( A  \  B ) ) )
18173expia 1209 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  Fn  A  /\  ( A  \  B ) 
C_  A )  -> 
( y  e.  ( A  \  B )  ->  ( f `  y )  e.  ( f " ( A 
\  B ) ) ) )
1915, 16, 18sylancl 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  (
f `  y )  e.  ( f " ( A  \  B ) ) ) )
20 dff1o3 5818 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : A -1-1-onto-> x  <->  ( f : A -onto-> x  /\  Fun  `' f ) )
2120simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : A -1-1-onto-> x  ->  Fun  `' f )
22 imadif 5656 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Fun  `' f  ->  ( f
" ( A  \  B ) )  =  ( ( f " A )  \  (
f " B ) ) )
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : A -1-1-onto-> x  ->  ( f
" ( A  \  B ) )  =  ( ( f " A )  \  (
f " B ) ) )
2423eleq2d 2513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : A -1-1-onto-> x  ->  ( ( f `  y )  e.  ( f "
( A  \  B
) )  <->  ( f `  y )  e.  ( ( f " A
)  \  ( f " B ) ) ) )
2519, 24sylibd 218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  (
f `  y )  e.  ( ( f " A )  \  (
f " B ) ) ) )
26 n0i 3735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  y )  e.  ( ( f
" A )  \ 
( f " B
) )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
2725, 26syl6 34 . . . . . . . . . . . . . . . . . . . 20  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) ) )
2814, 27syl5bir 222 . . . . . . . . . . . . . . . . . . 19  |-  ( f : A -1-1-onto-> x  ->  ( ( y  e.  A  /\  -.  y  e.  B
)  ->  -.  (
( f " A
)  \  ( f " B ) )  =  (/) ) )
2928exlimdv 1778 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  ( E. y ( y  e.  A  /\  -.  y  e.  B )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) ) )
3029imp 431 . . . . . . . . . . . . . . . . 17  |-  ( ( f : A -1-1-onto-> x  /\  E. y ( y  e.  A  /\  -.  y  e.  B ) )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
3113, 30sylan2 477 . . . . . . . . . . . . . . . 16  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
32 ssdif0 3822 . . . . . . . . . . . . . . . 16  |-  ( ( f " A ) 
C_  ( f " B )  <->  ( (
f " A ) 
\  ( f " B ) )  =  (/) )
3331, 32sylnibr 307 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  -.  ( f " A
)  C_  ( f " B ) )
34 dfpss3 3518 . . . . . . . . . . . . . . 15  |-  ( ( f " B ) 
C.  ( f " A )  <->  ( (
f " B ) 
C_  ( f " A )  /\  -.  ( f " A
)  C_  ( f " B ) ) )
3512, 33, 34sylanbrc 669 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C.  ( f " A ) )
36 imadmrn 5177 . . . . . . . . . . . . . . . . 17  |-  ( f
" dom  f )  =  ran  f
37 f1odm 5816 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  dom  f  =  A )
3837imaeq2d 5167 . . . . . . . . . . . . . . . . 17  |-  ( f : A -1-1-onto-> x  ->  ( f
" dom  f )  =  ( f " A ) )
39 f1ofo 5819 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  f : A -onto-> x )
40 forn 5794 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -onto-> x  ->  ran  f  =  x
)
4139, 40syl 17 . . . . . . . . . . . . . . . . 17  |-  ( f : A -1-1-onto-> x  ->  ran  f  =  x )
4236, 38, 413eqtr3a 2508 . . . . . . . . . . . . . . . 16  |-  ( f : A -1-1-onto-> x  ->  ( f
" A )  =  x )
4342psseq2d 3525 . . . . . . . . . . . . . . 15  |-  ( f : A -1-1-onto-> x  ->  ( ( f " B ) 
C.  ( f " A )  <->  ( f " B )  C.  x
) )
4443adantr 467 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( ( f " B )  C.  (
f " A )  <-> 
( f " B
)  C.  x )
)
4535, 44mpbid 214 . . . . . . . . . . . . 13  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C.  x )
46 php 7753 . . . . . . . . . . . . 13  |-  ( ( x  e.  om  /\  ( f " B
)  C.  x )  ->  -.  x  ~~  (
f " B ) )
4745, 46sylan2 477 . . . . . . . . . . . 12  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  -.  x  ~~  ( f " B
) )
48 f1of1 5811 . . . . . . . . . . . . . . . 16  |-  ( f : A -1-1-onto-> x  ->  f : A -1-1-> x )
49 f1ores 5826 . . . . . . . . . . . . . . . 16  |-  ( ( f : A -1-1-> x  /\  B  C_  A )  ->  ( f  |`  B ) : B -1-1-onto-> (
f " B ) )
5048, 4, 49syl2an 480 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f  |`  B ) : B -1-1-onto-> ( f " B
) )
51 vex 3047 . . . . . . . . . . . . . . . . . 18  |-  f  e. 
_V
5251resex 5147 . . . . . . . . . . . . . . . . 17  |-  ( f  |`  B )  e.  _V
53 f1oeq1 5803 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( f  |`  B )  ->  (
y : B -1-1-onto-> ( f
" B )  <->  ( f  |`  B ) : B -1-1-onto-> (
f " B ) ) )
5452, 53spcev 3140 . . . . . . . . . . . . . . . 16  |-  ( ( f  |`  B ) : B -1-1-onto-> ( f " B
)  ->  E. y 
y : B -1-1-onto-> ( f
" B ) )
55 bren 7575 . . . . . . . . . . . . . . . 16  |-  ( B 
~~  ( f " B )  <->  E. y 
y : B -1-1-onto-> ( f
" B ) )
5654, 55sylibr 216 . . . . . . . . . . . . . . 15  |-  ( ( f  |`  B ) : B -1-1-onto-> ( f " B
)  ->  B  ~~  ( f " B
) )
5750, 56syl 17 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  B  ~~  ( f " B ) )
58 entr 7618 . . . . . . . . . . . . . . 15  |-  ( ( x  ~~  B  /\  B  ~~  ( f " B ) )  ->  x  ~~  ( f " B ) )
5958expcom 437 . . . . . . . . . . . . . 14  |-  ( B 
~~  ( f " B )  ->  (
x  ~~  B  ->  x 
~~  ( f " B ) ) )
6057, 59syl 17 . . . . . . . . . . . . 13  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( x  ~~  B  ->  x  ~~  ( f
" B ) ) )
6160adantl 468 . . . . . . . . . . . 12  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  ( x  ~~  B  ->  x  ~~  ( f " B
) ) )
6247, 61mtod 181 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  -.  x  ~~  B )
6362exp32 609 . . . . . . . . . 10  |-  ( x  e.  om  ->  (
f : A -1-1-onto-> x  -> 
( B  C.  A  ->  -.  x  ~~  B
) ) )
6463exlimdv 1778 . . . . . . . . 9  |-  ( x  e.  om  ->  ( E. f  f : A
-1-1-onto-> x  ->  ( B  C.  A  ->  -.  x  ~~  B ) ) )
659, 64syl5bi 221 . . . . . . . 8  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C.  A  ->  -.  x  ~~  B ) ) )
6665imp31 434 . . . . . . 7  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  -.  x  ~~  B )
67 entr 7618 . . . . . . . . . 10  |-  ( ( B  ~~  A  /\  A  ~~  x )  ->  B  ~~  x )
6867ex 436 . . . . . . . . 9  |-  ( B 
~~  A  ->  ( A  ~~  x  ->  B  ~~  x ) )
69 ensym 7615 . . . . . . . . 9  |-  ( B 
~~  x  ->  x  ~~  B )
7068, 69syl6com 36 . . . . . . . 8  |-  ( A 
~~  x  ->  ( B  ~~  A  ->  x  ~~  B ) )
7170ad2antlr 732 . . . . . . 7  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  ( B  ~~  A  ->  x  ~~  B ) )
7266, 71mtod 181 . . . . . 6  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  -.  B  ~~  A )
73 brsdom 7589 . . . . . 6  |-  ( B 
~<  A  <->  ( B  ~<_  A  /\  -.  B  ~~  A ) )
748, 72, 73sylanbrc 669 . . . . 5  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  B  ~<  A )
7574exp31 608 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C.  A  ->  B  ~<  A ) ) )
7675rexlimiv 2872 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C.  A  ->  B  ~<  A ) )
771, 76sylbi 199 . 2  |-  ( A  e.  Fin  ->  ( B  C.  A  ->  B  ~<  A ) )
7877imp 431 1  |-  ( ( A  e.  Fin  /\  B  C.  A )  ->  B  ~<  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1443   E.wex 1662    e. wcel 1886   E.wrex 2737   _Vcvv 3044    \ cdif 3400    C_ wss 3403    C. wpss 3404   (/)c0 3730   class class class wbr 4401   `'ccnv 4832   dom cdm 4833   ran crn 4834    |` cres 4835   "cima 4836   Fun wfun 5575    Fn wfn 5576   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580   ` cfv 5581   omcom 6689    ~~ cen 7563    ~<_ cdom 7564    ~< csdm 7565   Fincfn 7566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-om 6690  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570
This theorem is referenced by:  pssinf  7779  f1finf1o  7795  findcard3  7811  fofinf1o  7849  ackbij1b  8666  fincssdom  8750  fin23lem25  8751  canthp1lem2  9075  pwfseqlem4  9084  uzindi  12191  symggen  17104  pgpssslw  17259  pgpfaclem2  17708  ppiltx  24097  finminlem  30967
  Copyright terms: Public domain W3C validator