Theorem bren 7421

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 7417	. . 3 |- Rel ~~
2		brrelex12 4976	. . 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 5742	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
5		fndm 5610	. . . . . 6 |- ( f Fn A -> dom f = A )
6		vex 3073	. . . . . . 7 |- f e. _V
7	6	dmex 6613	. . . . . 6 |- dom f e. _V
8	5, 7	syl6eqelr 2548	. . . . 5 |- ( f Fn A -> A e. _V )
9	4, 8	syl 16	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
10		f1ofo 5748	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
11		forn 5723	. . . . . 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 6614	. . . . 5 |- ran f e. _V
14	12, 13	syl6eqelr 2548	. . . 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 1689	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
17		f1oeq2 5733	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
18	17	exbidv 1681	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
19		f1oeq3 5734	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
20	19	exbidv 1681	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
21		df-en 7413	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
22	18, 20, 21	brabg 4708	. 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 1370   E.wex 1587   e. wcel 1758   _Vcvv 3070   class class class wbr 4392   dom cdm 4940   ran crn 4941   Rel wrel 4945   Fn wfn 5513   -onto->wfo 5516   -1-1-onto->wf1o 5517   ~~ cen 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pr 4631  ax-un 6474

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-xp 4946  df-rel 4947  df-cnv 4948  df-dm 4950  df-rn 4951  df-fn 5521  df-f 5522  df-f1 5523  df-fo 5524  df-f1o 5525  df-en 7413

This theorem is referenced by:  domen  7425  f1oen3g  7427  ener  7458  en0  7474  ensn1  7475  en1  7478  unen  7494  enfixsn  7522  canth2  7566  mapen  7577  ssenen  7587  phplem4  7595  php3  7599  isinf  7629  ssfi  7636  domunfican  7687  fiint  7691  mapfien2  7761  unxpwdom2  7906  isinffi  8265  infxpenc2  8291  infxpenc2OLD  8295  fseqen  8300  dfac8b  8304  infpwfien  8335  dfac12r  8418  infmap2  8490  cff1  8530  infpssr  8580  fin4en1  8581  enfin2i  8593  enfin1ai  8656  axcc3  8710  axcclem  8729  numth  8744  ttukey2g  8788  canthnum  8919  canthwe  8921  canthp1  8924  pwfseq  8934  tskuni  9053  gruen  9082  hasheqf1o  12223  hashfacen  12311  fz1f1o  13291  ruc  13629  cnso  13633  eulerth  13962  ablfaclem3  16695  lbslcic  18381  uvcendim  18387  indishmph  19489  ufldom  19653  ovolctb  21091  ovoliunlem3  21105  iunmbl2  21156  dyadmbl  21198  vitali  21211  nbusgrafi  23494  cusgrafilem3  23526  volmeas  26783  eulerpart  26901  derangenlem  27195  mblfinlem1  28568  eldioph2lem1  29238  mapfien2OLD  29589  isnumbasgrplem1  29597  wlknwwlknen  30487