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

Theorem bren 7108
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 7105 . . 3  |-  Rel  ~~
2 brrelex12 4906 . . 3  |-  ( ( Rel  ~~  /\  A  ~~  B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
31, 2mpan 652 . 2  |-  ( A 
~~  B  ->  ( A  e.  _V  /\  B  e.  _V ) )
4 f1ofn 5666 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  f  Fn  A )
5 fndm 5535 . . . . . 6  |-  ( f  Fn  A  ->  dom  f  =  A )
6 vex 2951 . . . . . . 7  |-  f  e. 
_V
76dmex 5123 . . . . . 6  |-  dom  f  e.  _V
85, 7syl6eqelr 2524 . . . . 5  |-  ( f  Fn  A  ->  A  e.  _V )
94, 8syl 16 . . . 4  |-  ( f : A -1-1-onto-> B  ->  A  e.  _V )
10 f1ofo 5672 . . . . . 6  |-  ( f : A -1-1-onto-> B  ->  f : A -onto-> B )
11 forn 5647 . . . . . 6  |-  ( f : A -onto-> B  ->  ran  f  =  B
)
1210, 11syl 16 . . . . 5  |-  ( f : A -1-1-onto-> B  ->  ran  f  =  B )
136rnex 5124 . . . . 5  |-  ran  f  e.  _V
1412, 13syl6eqelr 2524 . . . 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 1644 . 2  |-  ( E. f  f : A -1-1-onto-> B  ->  ( A  e.  _V  /\  B  e.  _V )
)
17 f1oeq2 5657 . . . 4  |-  ( x  =  A  ->  (
f : x -1-1-onto-> y  <->  f : A
-1-1-onto-> y ) )
1817exbidv 1636 . . 3  |-  ( x  =  A  ->  ( E. f  f :
x
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> y ) )
19 f1oeq3 5658 . . . 4  |-  ( y  =  B  ->  (
f : A -1-1-onto-> y  <->  f : A
-1-1-onto-> B ) )
2019exbidv 1636 . . 3  |-  ( y  =  B  ->  ( E. f  f : A
-1-1-onto-> y 
<->  E. f  f : A -1-1-onto-> B ) )
21 df-en 7101 . . 3  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
2218, 20, 21brabg 4466 . 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 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948   class class class wbr 4204   dom cdm 4869   ran crn 4870   Rel wrel 4874    Fn wfn 5440   -onto->wfo 5443   -1-1-onto->wf1o 5444    ~~ cen 7097
This theorem is referenced by:  domen  7112  f1oen3g  7114  ener  7145  en0  7161  ensn1  7162  en1  7165  unen  7180  canth2  7251  mapen  7262  ssenen  7272  phplem4  7280  php3  7284  isinf  7313  ssfi  7320  domunfican  7370  fiint  7374  unxpwdom2  7545  isinffi  7868  infxpenc2  7892  fseqen  7897  dfac8b  7901  infpwfien  7932  dfac12r  8015  infmap2  8087  cff1  8127  infpssr  8177  fin4en1  8178  enfin2i  8190  enfin1ai  8253  axcc3  8307  axcclem  8326  numth  8341  ttukey2g  8385  canthnum  8513  canthwe  8515  canthp1  8518  pwfseq  8528  tskuni  8647  gruen  8676  hasheqf1o  11621  hashfacen  11691  fz1f1o  12492  ruc  12830  cnso  12834  eulerth  13160  ablfaclem3  15633  indishmph  17818  ufldom  17982  ovolctb  19374  ovoliunlem3  19388  iunmbl2  19439  dyadmbl  19480  vitali  19493  nbusgrafi  21446  cusgrafilem3  21478  volmeas  24575  derangenlem  24845  mblfinlem  26190  eldioph2lem1  26755  enfixsn  27172  mapfien2  27173  isnumbasgrplem1  27181  lbslcic  27226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-xp 4875  df-rel 4876  df-cnv 4877  df-dm 4879  df-rn 4880  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-en 7101
  Copyright terms: Public domain W3C validator