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

Theorem bren 6871
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 6868 . . 3  |-  Rel  ~~
2 brrelex12 4726 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 651 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5473 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5343 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2791 . . . . . . 7  |-  f  e. 
_V
76dmex 4941 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2372 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 15 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5479 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5454 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 15 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 4942 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2372 . . . 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 1666 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5464 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1612 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5465 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1612 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 6864 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4284 . 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 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788   class class class wbr 4023   dom cdm 4689   ran crn 4690   Rel wrel 4694    Fn wfn 5250   -onto->wfo 5253   -1-1-onto->wf1o 5254    ~~ cen 6860
This theorem is referenced by:  domen  6875  f1oen3g  6877  ener  6908  en0  6924  ensn1  6925  en1  6928  unen  6943  canth2  7014  mapen  7025  ssenen  7035  phplem4  7043  php3  7047  isinf  7076  ssfi  7083  domunfican  7129  fiint  7133  unxpwdom2  7302  isinffi  7625  infxpenc2  7649  fseqen  7654  dfac8b  7658  infpwfien  7689  dfac12r  7772  infmap2  7844  cff1  7884  infpssr  7934  fin4en1  7935  enfin2i  7947  enfin1ai  8010  axcc3  8064  axcclem  8083  numth  8099  ttukey2g  8143  canthnum  8271  canthwe  8273  canthp1  8276  pwfseq  8286  tskuni  8405  gruen  8434  hashfacen  11392  fz1f1o  12183  ruc  12521  cnso  12525  eulerth  12851  ablfaclem3  15322  indishmph  17489  ufldom  17657  ovolctb  18849  ovoliunlem3  18863  iunmbl2  18914  dyadmbl  18955  vitali  18968  derangenlem  23702  eldioph2lem1  26839  enfixsn  27257  mapfien2  27258  isnumbasgrplem1  27266  lbslcic  27311
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696  df-cnv 4697  df-dm 4699  df-rn 4700  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-en 6864
  Copyright terms: Public domain W3C validator