Theorem bren 8510

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 8509	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6609	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6448	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3496	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7608	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2920	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6615	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6586	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7609	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2920	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 514	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1925	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		f1oeq2 6598	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝑦))
16	15	exbidv 1916	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑦))
17		f1oeq3 6599	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑓:𝐴–1-1-onto→𝑦 ↔ 𝑓:𝐴–1-1-onto→𝐵))
18	17	exbidv 1916	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴–1-1-onto→𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
19		df-en 8502	. . 3 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
20	16, 18, 19	brabg 5417	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
21	1, 14, 20	pm5.21nii 382	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108  Vcvv 3493   class class class wbr 5057  dom cdm 5548  ran crn 5549   Fn wfn 6343  –onto→wfo 6346  –1-1-onto→wf1o 6347   ≈ cen 8498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-dm 5558  df-rn 5559  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-en 8502

This theorem is referenced by:  domen  8514  f1oen3g  8517  ener  8548  en0  8564  ensn1  8565  en1  8568  unen  8588  enfixsn  8618  canth2  8662  mapen  8673  ssenen  8683  phplem4  8691  php3  8695  isinf  8723  ssfi  8730  domunfican  8783  fiint  8787  mapfien2  8864  unxpwdom2  9044  isinffi  9413  infxpenc2  9440  fseqen  9445  dfac8b  9449  infpwfien  9480  dfac12r  9564  infmap2  9632  cff1  9672  infpssr  9722  fin4en1  9723  enfin2i  9735  enfin1ai  9798  axcc3  9852  axcclem  9871  numth  9886  ttukey2g  9930  canthnum  10063  canthwe  10065  canthp1  10068  pwfseq  10078  tskuni  10197  gruen  10226  hasheqf1o  13701  hashfacen  13804  fz1f1o  15059  ruc  15588  cnso  15592  eulerth  16112  ablfaclem3  19201  lbslcic  20977  uvcendim  20983  indishmph  22398  ufldom  22562  ovolctb  24083  ovoliunlem3  24097  iunmbl2  24150  dyadmbl  24193  vitali  24206  cusgrfilem3  27231  padct  30447  f1ocnt  30517  volmeas  31483  eulerpart  31633  derangenlem  32411  mblfinlem1  34921  eldioph2lem1  39347  isnumbasgrplem1  39691  nnf1oxpnn  41446  sprsymrelen  43652  prproropen  43660  uspgrspren  44017  uspgrbisymrel  44019  rrx2xpreen  44696