Theorem bren 7522

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		relen 7518	. . 3 |- Rel ~~
2		brrelex12 5036	. . 3 |- ( ( Rel ~~ /\ A ~~ B ) -> ( A e. _V /\ B e. _V ) )
3	1, 2	mpan 670	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
4		f1ofn 5815	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
5		fndm 5678	. . . . . 6 |- ( f Fn A -> dom f = A )
6		vex 3116	. . . . . . 7 |- f e. _V
7	6	dmex 6714	. . . . . 6 |- dom f e. _V
8	5, 7	syl6eqelr 2564	. . . . 5 |- ( f Fn A -> A e. _V )
9	4, 8	syl 16	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
10		f1ofo 5821	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
11		forn 5796	. . . . . 6 |- ( f : A -onto-> B -> ran f = B )
12	10, 11	syl 16	. . . . 5 |- ( f : A -1-1-onto-> B -> ran f = B )
13	6	rnex 6715	. . . . 5 |- ran f e. _V
14	12, 13	syl6eqelr 2564	. . . 4 |- ( f : A -1-1-onto-> B -> B e. _V )
15	9, 14	jca 532	. . 3 |- ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
16	15	exlimiv 1698	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
17		f1oeq2 5806	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
18	17	exbidv 1690	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
19		f1oeq3 5807	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
20	19	exbidv 1690	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
21		df-en 7514	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
22	18, 20, 21	brabg 4766	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
23	3, 16, 22	pm5.21nii 353	1 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   _Vcvv 3113   class class class wbr 4447   dom cdm 4999   ran crn 5000   Rel wrel 5004   Fn wfn 5581   -onto->wfo 5584   -1-1-onto->wf1o 5585   ~~ cen 7510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-rel 5006  df-cnv 5007  df-dm 5009  df-rn 5010  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-en 7514

This theorem is referenced by:  domen  7526  f1oen3g  7528  ener  7559  en0  7575  ensn1  7576  en1  7579  unen  7595  enfixsn  7623  canth2  7667  mapen  7678  ssenen  7688  phplem4  7696  php3  7700  isinf  7730  ssfi  7737  domunfican  7789  fiint  7793  mapfien2  7864  unxpwdom2  8010  isinffi  8369  infxpenc2  8395  infxpenc2OLD  8399  fseqen  8404  dfac8b  8408  infpwfien  8439  dfac12r  8522  infmap2  8594  cff1  8634  infpssr  8684  fin4en1  8685  enfin2i  8697  enfin1ai  8760  axcc3  8814  axcclem  8833  numth  8848  ttukey2g  8892  canthnum  9023  canthwe  9025  canthp1  9028  pwfseq  9038  tskuni  9157  gruen  9186  hasheqf1o  12386  hashfacen  12465  fz1f1o  13491  ruc  13833  cnso  13837  eulerth  14168  ablfaclem3  16928  lbslcic  18643  uvcendim  18649  indishmph  20034  ufldom  20198  ovolctb  21636  ovoliunlem3  21650  iunmbl2  21702  dyadmbl  21744  vitali  21757  nbusgrafi  24124  cusgrafilem3  24157  wlknwwlknen  24391  volmeas  27843  eulerpart  27961  derangenlem  28255  mblfinlem1  29628  eldioph2lem1  30297  mapfien2OLD  30646  isnumbasgrplem1  30654