Theorem bren 6858

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 6856	. 2 |- ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2		f1ofn 5545	. . . . 5 |- ( f : A -1-1-onto-> B -> f Fn A )
3		fndm 5392	. . . . . 6 |- ( f Fn A -> dom f = A )
4		vex 2779	. . . . . . 7 |- f e. _V
5	4	dmex 4964	. . . . . 6 |- dom f e. _V
6	3, 5	eqeltrrdi 2299	. . . . 5 |- ( f Fn A -> A e. _V )
7	2, 6	syl 14	. . . 4 |- ( f : A -1-1-onto-> B -> A e. _V )
8		f1ofo 5551	. . . . . 6 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
9		forn 5523	. . . . . 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 4965	. . . . 5 |- ran f e. _V
12	10, 11	eqeltrrdi 2299	. . . 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 1622	. 2 |- ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15		f1oeq2 5533	. . . 4 |- ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16	15	exbidv 1849	. . 3 |- ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17		f1oeq3 5534	. . . 4 |- ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18	17	exbidv 1849	. . 3 |- ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19		df-en 6851	. . 3 |- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20	16, 18, 19	brabg 4333	. 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 1516   e. wcel 2178   _Vcvv 2776   class class class wbr 4059   dom cdm 4693   ran crn 4694   Fn wfn 5285   -onto->wfo 5288   -1-1-onto->wf1o 5289   ~~ cen 6848

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-xp 4699  df-rel 4700  df-cnv 4701  df-dm 4703  df-rn 4704  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297  df-en 6851

This theorem is referenced by:  domen  6863  f1oen3g  6868  ener  6894  en0  6910  ensn1  6911  en1  6914  unen  6932  en2  6936  enm  6940  xpen  6967  mapen  6968  ssenen  6973  phplem4  6977  phplem4on  6990  fidceq  6992  dif1en  7002  fin0  7008  fin0or  7009  en2eqpr  7030  fiintim  7054  fidcenumlemim  7080  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  pr2cv1  7329  cc3  7415  hasheqf1o  10967  hashfacen  11018  fz1f1o  11801  nninfct  12477  eulerth  12670  ennnfonelemim  12910  exmidunben  12912  ctinfom  12914  qnnen  12917  enctlem  12918  ctiunct  12926  exmidsbthrlem  16163  sbthom  16167