Theorem bren 6835

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 6833	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2		f1ofn 5523	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
3		fndm 5373	. . . . . 6 |- ( f Fn A -> dom f = A )
4		vex 2775	. . . . . . 7 |- f e. _V
5	4	dmex 4945	. . . . . 6 |- dom f e. _V
6	3, 5	eqeltrrdi 2297	. . . . 5 |- ( f Fn A -> A e. _V )
7	2, 6	syl 14	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
8		f1ofo 5529	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
9		forn 5501	. . . . . 6 |- ( f : A -onto-> B -> ran f = B )
10	8, 9	syl 14	. . . . 5 |- ( f : A -1-1-onto-> B -> ran f = B )
11	4	rnex 4946	. . . . 5 |- ran f e. _V
12	10, 11	eqeltrrdi 2297	. . . 4 |- ( f : A -1-1-onto-> B -> B e. _V )
13	7, 12	jca 306	. . 3 |- ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
14	13	exlimiv 1621	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15		f1oeq2 5511	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16	15	exbidv 1848	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17		f1oeq3 5512	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18	17	exbidv 1848	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19		df-en 6828	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20	16, 18, 19	brabg 4315	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
21	1, 14, 20	pm5.21nii 706	1 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   E.wex 1515   e. wcel 2176   _Vcvv 2772   class class class wbr 4044   dom cdm 4675   ran crn 4676   Fn wfn 5266   -onto->wfo 5269   -1-1-onto->wf1o 5270   ~~ cen 6825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-xp 4681  df-rel 4682  df-cnv 4683  df-dm 4685  df-rn 4686  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-en 6828

This theorem is referenced by:  domen  6840  f1oen3g  6845  ener  6871  en0  6887  ensn1  6888  en1  6891  unen  6908  en2  6912  enm  6915  xpen  6942  mapen  6943  ssenen  6948  phplem4  6952  phplem4on  6964  fidceq  6966  dif1en  6976  fin0  6982  fin0or  6983  en2eqpr  7004  fiintim  7028  fidcenumlemim  7054  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  cc3  7380  hasheqf1o  10930  hashfacen  10981  fz1f1o  11686  nninfct  12362  eulerth  12555  ennnfonelemim  12795  exmidunben  12797  ctinfom  12799  qnnen  12802  enctlem  12803  ctiunct  12811  exmidsbthrlem  15961  sbthom  15965