Theorem bren 7964

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 7963	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2		f1ofn 6138	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
3		fndm 5990	. . . . . 6 |- ( f Fn A -> dom f = A )
4		vex 3203	. . . . . . 7 |- f e. _V
5	4	dmex 7099	. . . . . 6 |- dom f e. _V
6	3, 5	syl6eqelr 2710	. . . . 5 |- ( f Fn A -> A e. _V )
7	2, 6	syl 17	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
8		f1ofo 6144	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
9		forn 6118	. . . . . 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 7100	. . . . 5 |- ran f e. _V
12	10, 11	syl6eqelr 2710	. . . 4 |- ( f : A -1-1-onto-> B -> B e. _V )
13	7, 12	jca 554	. . 3 |- ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
14	13	exlimiv 1858	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15		f1oeq2 6128	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16	15	exbidv 1850	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17		f1oeq3 6129	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18	17	exbidv 1850	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19		df-en 7956	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20	16, 18, 19	brabg 4994	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
21	1, 14, 20	pm5.21nii 368	1 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Syntax hints:   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   class class class wbr 4653   dom cdm 5114   ran crn 5115   Fn wfn 5883   -onto->wfo 5886   -1-1-onto->wf1o 5887   ~~ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-en 7956

This theorem is referenced by:  domen  7968  f1oen3g  7971  ener  8002  enerOLD  8003  en0  8019  ensn1  8020  en1  8023  unen  8040  enfixsn  8069  canth2  8113  mapen  8124  ssenen  8134  phplem4  8142  php3  8146  isinf  8173  ssfi  8180  domunfican  8233  fiint  8237  mapfien2  8314  unxpwdom2  8493  isinffi  8818  infxpenc2  8845  fseqen  8850  dfac8b  8854  infpwfien  8885  dfac12r  8968  infmap2  9040  cff1  9080  infpssr  9130  fin4en1  9131  enfin2i  9143  enfin1ai  9206  axcc3  9260  axcclem  9279  numth  9294  ttukey2g  9338  canthnum  9471  canthwe  9473  canthp1  9476  pwfseq  9486  tskuni  9605  gruen  9634  hasheqf1o  13137  hashfacen  13238  fz1f1o  14441  ruc  14972  cnso  14976  eulerth  15488  ablfaclem3  18486  lbslcic  20180  uvcendim  20186  indishmph  21601  ufldom  21766  ovolctb  23258  ovoliunlem3  23272  iunmbl2  23325  dyadmbl  23368  vitali  23382  cusgrfilem3  26353  wlknwwlksnen  26779  padct  29497  f1ocnt  29559  volmeas  30294  eulerpart  30444  derangenlem  31153  mblfinlem1  33446  eldioph2lem1  37323  isnumbasgrplem1  37671  nnf1oxpnn  39384  sprsymrelen  41750  uspgrspren  41760  uspgrbisymrel  41762