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

Theorem bren 6956
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 6953 . . 3  |-  Rel  ~~
2 brrelex12 4805 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 651 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5553 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5422 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2867 . . . . . . 7  |-  f  e. 
_V
76dmex 5020 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2447 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 15 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5559 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5534 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 15 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 5021 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2447 . . . 4  |-  ( f : A -1-1-onto-> B  ->  B  e.  _V )
159, 14jca 518 . . 3  |-  ( f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e. 
_V ) )
1615exlimiv 1634 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5544 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1626 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5545 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1626 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 6949 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4363 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  ~~  B  <->  E. f  f : A -1-1-onto-> B
) )
233, 16, 22pm5.21nii 342 1  |-  ( A 
~~  B  <->  E. f 
f : A -1-1-onto-> B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1541    = wceq 1642    e. wcel 1710   _Vcvv 2864   class class class wbr 4102   dom cdm 4768   ran crn 4769   Rel wrel 4773    Fn wfn 5329   -onto->wfo 5332   -1-1-onto->wf1o 5333    ~~ cen 6945
This theorem is referenced by:  domen  6960  f1oen3g  6962  ener  6993  en0  7009  ensn1  7010  en1  7013  unen  7028  canth2  7099  mapen  7110  ssenen  7120  phplem4  7128  php3  7132  isinf  7161  ssfi  7168  domunfican  7216  fiint  7220  unxpwdom2  7389  isinffi  7712  infxpenc2  7736  fseqen  7741  dfac8b  7745  infpwfien  7776  dfac12r  7859  infmap2  7931  cff1  7971  infpssr  8021  fin4en1  8022  enfin2i  8034  enfin1ai  8097  axcc3  8151  axcclem  8170  numth  8186  ttukey2g  8230  canthnum  8358  canthwe  8360  canthp1  8363  pwfseq  8373  tskuni  8492  gruen  8521  hashfacen  11482  fz1f1o  12274  ruc  12612  cnso  12616  eulerth  12942  ablfaclem3  15415  indishmph  17589  ufldom  17753  ovolctb  18947  ovoliunlem3  18961  iunmbl2  19012  dyadmbl  19053  vitali  19066  volmeas  23851  derangenlem  24106  eldioph2lem1  26162  enfixsn  26580  mapfien2  26581  isnumbasgrplem1  26589  lbslcic  26634  hasheqf1o  27474  nbusgrafi  27604
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293  ax-un 4591
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-xp 4774  df-rel 4775  df-cnv 4776  df-dm 4778  df-rn 4779  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-en 6949
  Copyright terms: Public domain W3C validator