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

Theorem bren 7146
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 7143 . . 3  |-  Rel  ~~
2 brrelex12 4944 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 653 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5704 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5573 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2965 . . . . . . 7  |-  f  e. 
_V
76dmex 5161 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2531 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 16 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5710 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5685 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 16 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 5162 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2531 . . . 4  |-  ( f : A -1-1-onto-> B  ->  B  e.  _V )
159, 14jca 520 . . 3  |-  ( f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e. 
_V ) )
1615exlimiv 1645 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5695 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1637 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5696 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1637 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 7139 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4503 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  ~~  B  <->  E. f  f : A -1-1-onto-> B
) )
233, 16, 22pm5.21nii 344 1  |-  ( A 
~~  B  <->  E. f 
f : A -1-1-onto-> B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1727   _Vcvv 2962   class class class wbr 4237   dom cdm 4907   ran crn 4908   Rel wrel 4912    Fn wfn 5478   -onto->wfo 5481   -1-1-onto->wf1o 5482    ~~ cen 7135
This theorem is referenced by:  domen  7150  f1oen3g  7152  ener  7183  en0  7199  ensn1  7200  en1  7203  unen  7218  canth2  7289  mapen  7300  ssenen  7310  phplem4  7318  php3  7322  isinf  7351  ssfi  7358  domunfican  7408  fiint  7412  unxpwdom2  7585  isinffi  7910  infxpenc2  7934  fseqen  7939  dfac8b  7943  infpwfien  7974  dfac12r  8057  infmap2  8129  cff1  8169  infpssr  8219  fin4en1  8220  enfin2i  8232  enfin1ai  8295  axcc3  8349  axcclem  8368  numth  8383  ttukey2g  8427  canthnum  8555  canthwe  8557  canthp1  8560  pwfseq  8570  tskuni  8689  gruen  8718  hasheqf1o  11664  hashfacen  11734  fz1f1o  12535  ruc  12873  cnso  12877  eulerth  13203  ablfaclem3  15676  indishmph  17861  ufldom  18025  ovolctb  19417  ovoliunlem3  19431  iunmbl2  19482  dyadmbl  19523  vitali  19536  nbusgrafi  21489  cusgrafilem3  21521  volmeas  24618  derangenlem  24888  mblfinlem1  26279  eldioph2lem1  26856  enfixsn  27272  mapfien2  27273  isnumbasgrplem1  27281  lbslcic  27326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432  ax-un 4730
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-xp 4913  df-rel 4914  df-cnv 4915  df-dm 4917  df-rn 4918  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-en 7139
  Copyright terms: Public domain W3C validator