Theorem bren 7586

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 7585	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2		f1ofn 5832	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
3		fndm 5693	. . . . . 6 |- ( f Fn A -> dom f = A )
4		vex 3090	. . . . . . 7 |- f e. _V
5	4	dmex 6740	. . . . . 6 |- dom f e. _V
6	3, 5	syl6eqelr 2526	. . . . 5 |- ( f Fn A -> A e. _V )
7	2, 6	syl 17	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
8		f1ofo 5838	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
9		forn 5813	. . . . . 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 6741	. . . . 5 |- ran f e. _V
12	10, 11	syl6eqelr 2526	. . . 4 |- ( f : A -1-1-onto-> B -> B e. _V )
13	7, 12	jca 534	. . 3 |- ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
14	13	exlimiv 1769	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15		f1oeq2 5823	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16	15	exbidv 1761	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17		f1oeq3 5824	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18	17	exbidv 1761	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19		df-en 7578	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20	16, 18, 19	brabg 4740	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
21	1, 14, 20	pm5.21nii 354	1 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Syntax hints:   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1870   _Vcvv 3087   class class class wbr 4426   dom cdm 4854   ran crn 4855   Fn wfn 5596   -onto->wfo 5599   -1-1-onto->wf1o 5600   ~~ cen 7574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-xp 4860  df-rel 4861  df-cnv 4862  df-dm 4864  df-rn 4865  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-en 7578

This theorem is referenced by:  domen  7590  f1oen3g  7592  ener  7623  en0  7639  ensn1  7640  en1  7643  unen  7659  enfixsn  7687  canth2  7731  mapen  7742  ssenen  7752  phplem4  7760  php3  7764  isinf  7791  ssfi  7798  domunfican  7850  fiint  7854  mapfien2  7928  unxpwdom2  8103  isinffi  8425  infxpenc2  8451  fseqen  8456  dfac8b  8460  infpwfien  8491  dfac12r  8574  infmap2  8646  cff1  8686  infpssr  8736  fin4en1  8737  enfin2i  8749  enfin1ai  8812  axcc3  8866  axcclem  8885  numth  8900  ttukey2g  8944  canthnum  9073  canthwe  9075  canthp1  9078  pwfseq  9088  tskuni  9207  gruen  9236  hasheqf1o  12529  hashfacen  12612  fz1f1o  13754  ruc  14273  cnso  14277  eulerth  14700  ablfaclem3  17659  lbslcic  19334  uvcendim  19340  indishmph  20748  ufldom  20912  ovolctb  22328  ovoliunlem3  22342  iunmbl2  22395  dyadmbl  22443  vitali  22456  nbusgrafi  25029  cusgrafilem3  25062  wlknwwlknen  25296  padct  28158  f1ocnt  28220  volmeas  28901  eulerpart  29049  derangenlem  29690  mblfinlem1  31692  eldioph2lem1  35322  isnumbasgrplem1  35681