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

Theorem hashen 11559
Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
Assertion
Ref Expression
hashen  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  <->  A  ~~  B ) )

Proof of Theorem hashen
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 fveq2 5669 . . . 4  |-  ( (
# `  A )  =  ( # `  B
)  ->  ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( # `  A ) )  =  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( # `  B
) ) )
2 eqid 2388 . . . . . 6  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om )
32hashginv 11550 . . . . 5  |-  ( A  e.  Fin  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( # `  A
) )  =  (
card `  A )
)
42hashginv 11550 . . . . 5  |-  ( B  e.  Fin  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( # `  B
) )  =  (
card `  B )
)
53, 4eqeqan12d 2403 . . . 4  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( # `  A ) )  =  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( # `  B
) )  <->  ( card `  A )  =  (
card `  B )
) )
61, 5syl5ib 211 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  ->  ( card `  A )  =  ( card `  B
) ) )
7 fveq2 5669 . . . 4  |-  ( (
card `  A )  =  ( card `  B
)  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  A
) )  =  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) ) )
82hashgval 11549 . . . . 5  |-  ( A  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  =  ( # `  A
) )
92hashgval 11549 . . . . 5  |-  ( B  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) )  =  ( # `  B
) )
108, 9eqeqan12d 2403 . . . 4  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  A
) )  =  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) )  <-> 
( # `  A )  =  ( # `  B
) ) )
117, 10syl5ib 211 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  =  ( card `  B )  ->  ( # `
 A )  =  ( # `  B
) ) )
126, 11impbid 184 . 2  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  <->  ( card `  A )  =  (
card `  B )
) )
13 finnum 7769 . . 3  |-  ( A  e.  Fin  ->  A  e.  dom  card )
14 finnum 7769 . . 3  |-  ( B  e.  Fin  ->  B  e.  dom  card )
15 carden2 7808 . . 3  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  =  (
card `  B )  <->  A 
~~  B ) )
1613, 14, 15syl2an 464 . 2  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  =  ( card `  B )  <->  A  ~~  B ) )
1712, 16bitrd 245 1  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  <->  A  ~~  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2900   class class class wbr 4154    e. cmpt 4208   omcom 4786   `'ccnv 4818   dom cdm 4819    |` cres 4821   ` cfv 5395  (class class class)co 6021   reccrdg 6604    ~~ cen 7043   Fincfn 7046   cardccrd 7756   0cc0 8924   1c1 8925    + caddc 8927   #chash 11546
This theorem is referenced by:  hasheni  11560  hasheqf1o  11561  hashf1rn  11564  hasheq0  11572  hashsng  11575  hashsdom  11583  hash1snb  11609  hash2pr  11615  hashxplem  11624  hashmap  11626  hashpw  11627  hashbclem  11629  isercolllem2  12387  isercoll  12389  fz1f1o  12432  summolem3  12436  summolem2a  12437  mertenslem1  12589  hashdvds  13092  crt  13095  phimullem  13096  eulerth  13100  4sqlem11  13251  lagsubg2  14929  orbsta2  15019  dfod2  15128  sylow1lem2  15161  sylow2alem2  15180  sylow2a  15181  slwhash  15186  sylow2  15188  sylow3lem1  15189  cyggenod  15422  lt6abl  15432  gsumval3  15442  ablfac1c  15557  ablfac1eu  15559  ablfaclem3  15573  fta1blem  19959  vieta1  20097  basellem5  20735  isppw  20765  eupai  21538  derangen2  24640  subfacp1lem3  24648  subfacp1lem5  24650  erdsze2lem1  24669  erdsze2lem2  24670  prodmolem3  25039  prodmolem2a  25040  bpolylem  25809  eldioph2lem1  26510  frlmpwfi  26932  isnumbasgrplem3  26940  idomsubgmo  27184
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-cnex 8980  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-mulcom 8988  ax-addass 8989  ax-mulass 8990  ax-distr 8991  ax-i2m1 8992  ax-1ne0 8993  ax-1rid 8994  ax-rnegex 8995  ax-rrecex 8996  ax-cnre 8997  ax-pre-lttri 8998  ax-pre-lttrn 8999  ax-pre-ltadd 9000  ax-pre-mulgt0 9001
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-reu 2657  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-int 3994  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529  df-om 4787  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-riota 6486  df-recs 6570  df-rdg 6605  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-fin 7050  df-card 7760  df-pnf 9056  df-mnf 9057  df-xr 9058  df-ltxr 9059  df-le 9060  df-sub 9226  df-neg 9227  df-nn 9934  df-n0 10155  df-z 10216  df-uz 10422  df-hash 11547
  Copyright terms: Public domain W3C validator