Theorem bren 7604

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.

Step	Hyp	Ref	Expression
1		encv 7603	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2		f1ofn 5838	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
3		fndm 5697	. . . . . 6 |- ( f Fn A -> dom f = A )
4		vex 3060	. . . . . . 7 |- f e. _V
5	4	dmex 6753	. . . . . 6 |- dom f e. _V
6	3, 5	syl6eqelr 2549	. . . . 5 |- ( f Fn A -> A e. _V )
7	2, 6	syl 17	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
8		f1ofo 5844	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
9		forn 5819	. . . . . 6 |- ( f : A -onto-> B -> ran f = B )
10	8, 9	syl 17	. . . . 5 |- ( f : A -1-1-onto-> B -> ran f = B )
11	4	rnex 6754	. . . . 5 |- ran f e. _V
12	10, 11	syl6eqelr 2549	. . . 4 |- ( f : A -1-1-onto-> B -> B e. _V )
13	7, 12	jca 539	. . 3 |- ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
14	13	exlimiv 1787	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15		f1oeq2 5829	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16	15	exbidv 1779	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17		f1oeq3 5830	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18	17	exbidv 1779	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19		df-en 7596	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20	16, 18, 19	brabg 4734	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
21	1, 14, 20	pm5.21nii 359	1 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1455   E.wex 1674   e. wcel 1898   _Vcvv 3057   class class class wbr 4416   dom cdm 4853   ran crn 4854   Fn wfn 5596   -onto->wfo 5599   -1-1-onto->wf1o 5600   ~~ cen 7592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-en 7596

This theorem is referenced by:  domen  7608  f1oen3g  7611  ener  7642  en0  7658  ensn1  7659  en1  7662  unen  7678  enfixsn  7707  canth2  7751  mapen  7762  ssenen  7772  phplem4  7780  php3  7784  isinf  7811  ssfi  7818  domunfican  7870  fiint  7874  mapfien2  7948  unxpwdom2  8129  isinffi  8452  infxpenc2  8479  fseqen  8484  dfac8b  8488  infpwfien  8519  dfac12r  8602  infmap2  8674  cff1  8714  infpssr  8764  fin4en1  8765  enfin2i  8777  enfin1ai  8840  axcc3  8894  axcclem  8913  numth  8928  ttukey2g  8972  canthnum  9100  canthwe  9102  canthp1  9105  pwfseq  9115  tskuni  9234  gruen  9263  hasheqf1o  12564  hashfacen  12650  fz1f1o  13825  ruc  14344  cnso  14348  eulerth  14780  ablfaclem3  17769  lbslcic  19448  uvcendim  19454  indishmph  20862  ufldom  21026  ovolctb  22492  ovoliunlem3  22506  iunmbl2  22559  dyadmbl  22607  vitali  22620  nbusgrafi  25225  cusgrafilem3  25258  wlknwwlknen  25492  padct  28356  f1ocnt  28425  volmeas  29103  eulerpart  29264  derangenlem  29943  mblfinlem1  32022  eldioph2lem1  35647  isnumbasgrplem1  36005  nnf1oxpnn  37510  cusgrfilem3  39568