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

Theorem bren 7055
Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
Assertion
Ref Expression
bren  |-  ( A 
~~  B  <->  E. f 
f : A -1-1-onto-> B )
Distinct variable groups:    A, f    B, f

Proof of Theorem bren
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relen 7052 . . 3  |-  Rel  ~~
2 brrelex12 4857 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 652 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5617 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5486 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2904 . . . . . . 7  |-  f  e. 
_V
76dmex 5074 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2478 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 16 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5623 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5598 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 16 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 5075 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2478 . . . 4  |-  ( f : A -1-1-onto-> B  ->  B  e.  _V )
159, 14jca 519 . . 3  |-  ( f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e. 
_V ) )
1615exlimiv 1641 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5608 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1633 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5609 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1633 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 7048 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4417 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  ~~  B  <->  E. f  f : A -1-1-onto-> B
) )
233, 16, 22pm5.21nii 343 1  |-  ( A 
~~  B  <->  E. f 
f : A -1-1-onto-> B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1717   _Vcvv 2901   class class class wbr 4155   dom cdm 4820   ran crn 4821   Rel wrel 4825    Fn wfn 5391   -onto->wfo 5394   -1-1-onto->wf1o 5395    ~~ cen 7044
This theorem is referenced by:  domen  7059  f1oen3g  7061  ener  7092  en0  7108  ensn1  7109  en1  7112  unen  7127  canth2  7198  mapen  7209  ssenen  7219  phplem4  7227  php3  7231  isinf  7260  ssfi  7267  domunfican  7317  fiint  7321  unxpwdom2  7491  isinffi  7814  infxpenc2  7838  fseqen  7843  dfac8b  7847  infpwfien  7878  dfac12r  7961  infmap2  8033  cff1  8073  infpssr  8123  fin4en1  8124  enfin2i  8136  enfin1ai  8199  axcc3  8253  axcclem  8272  numth  8287  ttukey2g  8331  canthnum  8459  canthwe  8461  canthp1  8464  pwfseq  8474  tskuni  8593  gruen  8622  hasheqf1o  11562  hashfacen  11632  fz1f1o  12433  ruc  12771  cnso  12775  eulerth  13101  ablfaclem3  15574  indishmph  17753  ufldom  17917  ovolctb  19255  ovoliunlem3  19269  iunmbl2  19320  dyadmbl  19361  vitali  19374  nbusgrafi  21326  cusgrafilem3  21358  volmeas  24383  derangenlem  24638  eldioph2lem1  26511  enfixsn  26928  mapfien2  26929  isnumbasgrplem1  26937  lbslcic  26982
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 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-xp 4826  df-rel 4827  df-cnv 4828  df-dm 4830  df-rn 4831  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-en 7048
  Copyright terms: Public domain W3C validator