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

Theorem bren 6873
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 6870 . . 3  |-  Rel  ~~
2 brrelex12 4728 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 651 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5475 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5345 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2793 . . . . . . 7  |-  f  e. 
_V
76dmex 4943 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2374 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 15 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5481 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5456 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 15 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 4944 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2374 . . . 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 1668 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5466 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1614 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5467 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1614 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 6866 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4286 . 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 1530    = wceq 1625    e. wcel 1686   _Vcvv 2790   class class class wbr 4025   dom cdm 4691   ran crn 4692   Rel wrel 4696    Fn wfn 5252   -onto->wfo 5255   -1-1-onto->wf1o 5256    ~~ cen 6862
This theorem is referenced by:  domen  6877  f1oen3g  6879  ener  6910  en0  6926  ensn1  6927  en1  6930  unen  6945  canth2  7016  mapen  7027  ssenen  7037  phplem4  7045  php3  7049  isinf  7078  ssfi  7085  domunfican  7131  fiint  7135  unxpwdom2  7304  isinffi  7627  infxpenc2  7651  fseqen  7656  dfac8b  7660  infpwfien  7691  dfac12r  7774  infmap2  7846  cff1  7886  infpssr  7936  fin4en1  7937  enfin2i  7949  enfin1ai  8012  axcc3  8066  axcclem  8085  numth  8101  ttukey2g  8145  canthnum  8273  canthwe  8275  canthp1  8278  pwfseq  8288  tskuni  8407  gruen  8436  hashfacen  11394  fz1f1o  12185  ruc  12523  cnso  12527  eulerth  12853  ablfaclem3  15324  indishmph  17491  ufldom  17659  ovolctb  18851  ovoliunlem3  18865  iunmbl2  18916  dyadmbl  18957  vitali  18970  derangenlem  23704  eldioph2lem1  26850  enfixsn  27268  mapfien2  27269  isnumbasgrplem1  27277  lbslcic  27322
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698  df-cnv 4699  df-dm 4701  df-rn 4702  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-en 6866
  Copyright terms: Public domain W3C validator