Theorem bren 8566

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)

Assertion

Ref	Expression
bren	⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem bren

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		encv 8565	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6621	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6440	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3402	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7644	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2842	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6627	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6595	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7645	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2842	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 515	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1937	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		f1oeq2 6609	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝑦))
16	15	exbidv 1928	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑦))
17		f1oeq3 6610	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑓:𝐴–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝐵))
18	17	exbidv 1928	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
19		df-en 8558	. . 3 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
20	16, 18, 19	brabg 5394	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
21	1, 14, 20	pm5.21nii 383	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1542  ∃wex 1786   ∈ wcel 2114  Vcvv 3398   class class class wbr 5030  dom cdm 5525  ran crn 5526   Fn wfn 6334  –onto→wfo 6337  –1-1-onto→wf1o 6338   ≈ cen 8554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7481

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-xp 5531  df-rel 5532  df-cnv 5533  df-dm 5535  df-rn 5536  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-en 8558

This theorem is referenced by:  domen  8570  f1oen3g  8573  ener  8604  en0  8620  en0OLD  8621  ensn1  8622  en1  8625  en2sn  8642  unen  8646  enfixsn  8677  canth2  8722  mapen  8733  ssenen  8743  phplem4  8751  php3  8755  rexdif1en  8762  dif1en  8763  ensymfib  8784  entrfil  8785  isinf  8812  ssfiOLD  8818  domunfican  8867  fiint  8871  mapfien2  8948  unxpwdom2  9127  isinffi  9496  infxpenc2  9524  fseqen  9529  dfac8b  9533  infpwfien  9564  dfac12r  9648  infmap2  9720  cff1  9760  infpssr  9810  fin4en1  9811  enfin2i  9823  enfin1ai  9886  axcc3  9940  axcclem  9959  numth  9974  ttukey2g  10018  canthnum  10151  canthwe  10153  canthp1  10156  pwfseq  10166  tskuni  10285  gruen  10314  hasheqf1o  13803  hashfacen  13906  hashfacenOLD  13907  fz1f1o  15162  ruc  15690  cnso  15694  eulerth  16222  ablfaclem3  19330  lbslcic  20659  uvcendim  20665  indishmph  22551  ufldom  22715  ovolctb  24244  ovoliunlem3  24258  iunmbl2  24311  dyadmbl  24354  vitali  24367  cusgrfilem3  27401  padct  30631  f1ocnt  30700  volmeas  31771  eulerpart  31921  derangenlem  32706  mblfinlem1  35459  sticksstones4  39733  eldioph2lem1  40176  isnumbasgrplem1  40520  nnf1oxpnn  42294  sprsymrelen  44515  prproropen  44523  uspgrspren  44877  uspgrbisymrel  44879  1aryenef  45554  2aryenef  45565  rrx2xpreen  45628