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

Theorem hashen 12341
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 5787 . . . 4  |-  ( (
# `  A )  =  ( # `  B
)  ->  ( `' ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( # `  A ) )  =  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( # `  B
) ) )
2 eqid 2392 . . . . . 6  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om )
32hashginv 12330 . . . . 5  |-  ( A  e.  Fin  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( # `  A
) )  =  (
card `  A )
)
42hashginv 12330 . . . . 5  |-  ( B  e.  Fin  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( # `  B
) )  =  (
card `  B )
)
53, 4eqeqan12d 2415 . . . 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 219 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  ->  ( card `  A )  =  ( card `  B
) ) )
7 fveq2 5787 . . . 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 12329 . . . . 5  |-  ( A  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  =  ( # `  A
) )
92hashgval 12329 . . . . 5  |-  ( B  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) )  =  ( # `  B
) )
108, 9eqeqan12d 2415 . . . 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 219 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  =  ( card `  B )  ->  ( # `
 A )  =  ( # `  B
) ) )
126, 11impbid 191 . 2  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  <->  ( card `  A )  =  (
card `  B )
) )
13 finnum 8260 . . 3  |-  ( A  e.  Fin  ->  A  e.  dom  card )
14 finnum 8260 . . 3  |-  ( B  e.  Fin  ->  B  e.  dom  card )
15 carden2 8299 . . 3  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  =  (
card `  B )  <->  A 
~~  B ) )
1613, 14, 15syl2an 475 . 2  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  =  ( card `  B )  <->  A  ~~  B ) )
1712, 16bitrd 253 1  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  =  ( # `  B )  <->  A  ~~  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1836   _Vcvv 3047   class class class wbr 4380    |-> cmpt 4438   `'ccnv 4925   dom cdm 4926    |` cres 4928   ` cfv 5509  (class class class)co 6214   omcom 6617   reccrdg 7011    ~~ cen 7450   Fincfn 7453   cardccrd 8247   0cc0 9421   1c1 9422    + caddc 9424   #chash 12326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-recs 6978  df-rdg 7012  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-card 8251  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-nn 10471  df-n0 10731  df-z 10800  df-uz 11020  df-hash 12327
This theorem is referenced by:  hasheni  12342  hasheqf1o  12343  isfinite4  12354  hasheq0  12355  hashsng  12360  hashen1  12361  hashsdom  12371  hash1snb  12402  hashxplem  12414  hashmap  12416  hashpw  12417  hashbclem  12424  hash2pr  12438  pr2pwpr  12443  hash3tr  12452  isercolllem2  13509  isercoll  13511  fz1f1o  13553  summolem3  13557  summolem2a  13558  mertenslem1  13714  prodmolem3  13761  prodmolem2a  13762  hashdvds  14326  crt  14329  phimullem  14330  eulerth  14334  4sqlem11  14494  lagsubg2  16398  orbsta2  16488  dfod2  16722  sylow1lem2  16755  sylow2alem2  16774  sylow2a  16775  slwhash  16780  sylow2  16782  sylow3lem1  16783  cyggenod  17023  lt6abl  17033  gsumval3OLD  17044  gsumval3lem1  17045  gsumval3lem2  17046  gsumval3  17047  ablfac1c  17254  ablfac1eu  17256  ablfaclem3  17270  fta1blem  22673  vieta1  22812  basellem5  23494  isppw  23524  eupai  25109  derangen2  28843  subfacp1lem3  28851  subfacp1lem5  28853  erdsze2lem1  28872  erdsze2lem2  28873  bpolylem  29999  eldioph2lem1  30894  frlmpwfi  31250  isnumbasgrplem3  31258  idomsubgmo  31359
  Copyright terms: Public domain W3C validator