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

Theorem php3 7043
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 6881 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 relen 6864 . . . . . . . . 9  |-  Rel  ~~
32brrelexi 4728 . . . . . . . 8  |-  ( A 
~~  x  ->  A  e.  _V )
4 pssss 3272 . . . . . . . 8  |-  ( B 
C.  A  ->  B  C_  A )
5 ssdomg 6903 . . . . . . . . 9  |-  ( A  e.  _V  ->  ( B  C_  A  ->  B  ~<_  A ) )
65imp 418 . . . . . . . 8  |-  ( ( A  e.  _V  /\  B  C_  A )  ->  B  ~<_  A )
73, 4, 6syl2an 463 . . . . . . 7  |-  ( ( A  ~~  x  /\  B  C.  A )  ->  B  ~<_  A )
87adantll 694 . . . . . 6  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  B  ~<_  A )
9 bren 6867 . . . . . . . . 9  |-  ( A 
~~  x  <->  E. f 
f : A -1-1-onto-> x )
10 imass2 5048 . . . . . . . . . . . . . . . . 17  |-  ( B 
C_  A  ->  (
f " B ) 
C_  ( f " A ) )
114, 10syl 15 . . . . . . . . . . . . . . . 16  |-  ( B 
C.  A  ->  (
f " B ) 
C_  ( f " A ) )
1211adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C_  ( f " A ) )
13 pssnel 3520 . . . . . . . . . . . . . . . . 17  |-  ( B 
C.  A  ->  E. y
( y  e.  A  /\  -.  y  e.  B
) )
14 eldif 3163 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( A  \  B )  <->  ( y  e.  A  /\  -.  y  e.  B ) )
15 f1ofn 5439 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : A -1-1-onto-> x  ->  f  Fn  A )
16 difss 3304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A 
\  B )  C_  A
17 fnfvima 5718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  Fn  A  /\  ( A  \  B ) 
C_  A  /\  y  e.  ( A  \  B
) )  ->  (
f `  y )  e.  ( f " ( A  \  B ) ) )
18173expia 1153 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  Fn  A  /\  ( A  \  B ) 
C_  A )  -> 
( y  e.  ( A  \  B )  ->  ( f `  y )  e.  ( f " ( A 
\  B ) ) ) )
1915, 16, 18sylancl 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  (
f `  y )  e.  ( f " ( A  \  B ) ) ) )
20 dff1o3 5444 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : A -1-1-onto-> x  <->  ( f : A -onto-> x  /\  Fun  `' f ) )
2120simprbi 450 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : A -1-1-onto-> x  ->  Fun  `' f )
22 imadif 5293 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Fun  `' f  ->  ( f
" ( A  \  B ) )  =  ( ( f " A )  \  (
f " B ) ) )
2321, 22syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : A -1-1-onto-> x  ->  ( f
" ( A  \  B ) )  =  ( ( f " A )  \  (
f " B ) ) )
2423eleq2d 2351 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : A -1-1-onto-> x  ->  ( ( f `  y )  e.  ( f "
( A  \  B
) )  <->  ( f `  y )  e.  ( ( f " A
)  \  ( f " B ) ) ) )
2519, 24sylibd 205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  (
f `  y )  e.  ( ( f " A )  \  (
f " B ) ) ) )
26 n0i 3461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  y )  e.  ( ( f
" A )  \ 
( f " B
) )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
2725, 26syl6 29 . . . . . . . . . . . . . . . . . . . 20  |-  ( f : A -1-1-onto-> x  ->  ( y  e.  ( A  \  B )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) ) )
2814, 27syl5bir 209 . . . . . . . . . . . . . . . . . . 19  |-  ( f : A -1-1-onto-> x  ->  ( ( y  e.  A  /\  -.  y  e.  B
)  ->  -.  (
( f " A
)  \  ( f " B ) )  =  (/) ) )
2928exlimdv 1665 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  ( E. y ( y  e.  A  /\  -.  y  e.  B )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) ) )
3029imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( f : A -1-1-onto-> x  /\  E. y ( y  e.  A  /\  -.  y  e.  B ) )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
3113, 30sylan2 460 . . . . . . . . . . . . . . . 16  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  -.  ( ( f " A )  \  (
f " B ) )  =  (/) )
32 ssdif0 3514 . . . . . . . . . . . . . . . 16  |-  ( ( f " A ) 
C_  ( f " B )  <->  ( (
f " A ) 
\  ( f " B ) )  =  (/) )
3331, 32sylnibr 296 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  -.  ( f " A
)  C_  ( f " B ) )
34 dfpss3 3263 . . . . . . . . . . . . . . 15  |-  ( ( f " B ) 
C.  ( f " A )  <->  ( (
f " B ) 
C_  ( f " A )  /\  -.  ( f " A
)  C_  ( f " B ) ) )
3512, 33, 34sylanbrc 645 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C.  ( f " A ) )
36 imadmrn 5023 . . . . . . . . . . . . . . . . 17  |-  ( f
"  dom  f )  =  ran  f
37 f1odm 5442 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  dom  f  =  A )
3837imaeq2d 5011 . . . . . . . . . . . . . . . . 17  |-  ( f : A -1-1-onto-> x  ->  ( f
"  dom  f )  =  ( f " A ) )
39 f1ofo 5445 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -1-1-onto-> x  ->  f : A -onto-> x )
40 forn 5420 . . . . . . . . . . . . . . . . . 18  |-  ( f : A -onto-> x  ->  ran  f  =  x
)
4139, 40syl 15 . . . . . . . . . . . . . . . . 17  |-  ( f : A -1-1-onto-> x  ->  ran  f  =  x )
4236, 38, 413eqtr3a 2340 . . . . . . . . . . . . . . . 16  |-  ( f : A -1-1-onto-> x  ->  ( f
" A )  =  x )
4342psseq2d 3270 . . . . . . . . . . . . . . 15  |-  ( f : A -1-1-onto-> x  ->  ( ( f " B ) 
C.  ( f " A )  <->  ( f " B )  C.  x
) )
4443adantr 451 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( ( f " B )  C.  (
f " A )  <-> 
( f " B
)  C.  x )
)
4535, 44mpbid 201 . . . . . . . . . . . . 13  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f " B
)  C.  x )
46 php 7041 . . . . . . . . . . . . 13  |-  ( ( x  e.  om  /\  ( f " B
)  C.  x )  ->  -.  x  ~~  (
f " B ) )
4745, 46sylan2 460 . . . . . . . . . . . 12  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  -.  x  ~~  ( f " B
) )
48 f1of1 5437 . . . . . . . . . . . . . . . 16  |-  ( f : A -1-1-onto-> x  ->  f : A -1-1-> x )
49 f1ores 5453 . . . . . . . . . . . . . . . 16  |-  ( ( f : A -1-1-> x  /\  B  C_  A )  ->  ( f  |`  B ) : B -1-1-onto-> (
f " B ) )
5048, 4, 49syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( f  |`  B ) : B -1-1-onto-> ( f " B
) )
51 vex 2792 . . . . . . . . . . . . . . . . . 18  |-  f  e. 
_V
5251resex 4994 . . . . . . . . . . . . . . . . 17  |-  ( f  |`  B )  e.  _V
53 f1oeq1 5429 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( f  |`  B )  ->  (
y : B -1-1-onto-> ( f
" B )  <->  ( f  |`  B ) : B -1-1-onto-> (
f " B ) ) )
5452, 53spcev 2876 . . . . . . . . . . . . . . . 16  |-  ( ( f  |`  B ) : B -1-1-onto-> ( f " B
)  ->  E. y 
y : B -1-1-onto-> ( f
" B ) )
55 bren 6867 . . . . . . . . . . . . . . . 16  |-  ( B 
~~  ( f " B )  <->  E. y 
y : B -1-1-onto-> ( f
" B ) )
5654, 55sylibr 203 . . . . . . . . . . . . . . 15  |-  ( ( f  |`  B ) : B -1-1-onto-> ( f " B
)  ->  B  ~~  ( f " B
) )
5750, 56syl 15 . . . . . . . . . . . . . 14  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  ->  B  ~~  ( f " B ) )
58 entr 6909 . . . . . . . . . . . . . . 15  |-  ( ( x  ~~  B  /\  B  ~~  ( f " B ) )  ->  x  ~~  ( f " B ) )
5958expcom 424 . . . . . . . . . . . . . 14  |-  ( B 
~~  ( f " B )  ->  (
x  ~~  B  ->  x 
~~  ( f " B ) ) )
6057, 59syl 15 . . . . . . . . . . . . 13  |-  ( ( f : A -1-1-onto-> x  /\  B  C.  A )  -> 
( x  ~~  B  ->  x  ~~  ( f
" B ) ) )
6160adantl 452 . . . . . . . . . . . 12  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  ( x  ~~  B  ->  x  ~~  ( f " B
) ) )
6247, 61mtod 168 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( f : A -1-1-onto-> x  /\  B  C.  A ) )  ->  -.  x  ~~  B )
6362exp32 588 . . . . . . . . . 10  |-  ( x  e.  om  ->  (
f : A -1-1-onto-> x  -> 
( B  C.  A  ->  -.  x  ~~  B
) ) )
6463exlimdv 1665 . . . . . . . . 9  |-  ( x  e.  om  ->  ( E. f  f : A
-1-1-onto-> x  ->  ( B  C.  A  ->  -.  x  ~~  B ) ) )
659, 64syl5bi 208 . . . . . . . 8  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C.  A  ->  -.  x  ~~  B ) ) )
6665imp31 421 . . . . . . 7  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  -.  x  ~~  B )
67 entr 6909 . . . . . . . . . 10  |-  ( ( B  ~~  A  /\  A  ~~  x )  ->  B  ~~  x )
6867ex 423 . . . . . . . . 9  |-  ( B 
~~  A  ->  ( A  ~~  x  ->  B  ~~  x ) )
69 ensym 6906 . . . . . . . . 9  |-  ( B 
~~  x  ->  x  ~~  B )
7068, 69syl6com 31 . . . . . . . 8  |-  ( A 
~~  x  ->  ( B  ~~  A  ->  x  ~~  B ) )
7170ad2antlr 707 . . . . . . 7  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  ( B  ~~  A  ->  x  ~~  B ) )
7266, 71mtod 168 . . . . . 6  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  -.  B  ~~  A )
73 brsdom 6880 . . . . . 6  |-  ( B 
~<  A  <->  ( B  ~<_  A  /\  -.  B  ~~  A ) )
748, 72, 73sylanbrc 645 . . . . 5  |-  ( ( ( x  e.  om  /\  A  ~~  x )  /\  B  C.  A
)  ->  B  ~<  A )
7574exp31 587 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C.  A  ->  B  ~<  A ) ) )
7675rexlimiv 2662 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C.  A  ->  B  ~<  A ) )
771, 76sylbi 187 . 2  |-  ( A  e.  Fin  ->  ( B  C.  A  ->  B  ~<  A ) )
7877imp 418 1  |-  ( ( A  e.  Fin  /\  B  C.  A )  ->  B  ~<  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1685   E.wrex 2545   _Vcvv 2789    \ cdif 3150    C_ wss 3153    C. wpss 3154   (/)c0 3456   class class class wbr 4024   omcom 4655   `'ccnv 4687    dom cdm 4688   ran crn 4689    |` cres 4690   "cima 4691   Fun wfun 5215    Fn wfn 5216   -1-1->wf1 5218   -onto->wfo 5219   -1-1-onto->wf1o 5220   ` cfv 5221    ~~ cen 6856    ~<_ cdom 6857    ~< csdm 6858   Fincfn 6859
This theorem is referenced by:  pssinf  7069  f1finf1o  7082  findcard3  7096  fofinf1o  7133  ackbij1b  7861  fincssdom  7945  fin23lem25  7946  canthp1lem2  8271  pwfseqlem4  8280  uzindi  11039  pgpssslw  14921  pgpfaclem2  15313  ppiltx  20411  finminlem  25642  symggen  26822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-fin 6863
  Copyright terms: Public domain W3C validator