MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bren Structured version   Visualization version   GIF version

Theorem bren 8512
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.
StepHypRef Expression
1 encv 8511 . 2 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2 f1ofn 6611 . . . . 5 (𝑓:𝐴1-1-onto𝐵𝑓 Fn 𝐴)
3 fndm 6450 . . . . . 6 (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4 vex 3498 . . . . . . 7 𝑓 ∈ V
54dmex 7610 . . . . . 6 dom 𝑓 ∈ V
63, 5eqeltrrdi 2922 . . . . 5 (𝑓 Fn 𝐴𝐴 ∈ V)
72, 6syl 17 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐴 ∈ V)
8 f1ofo 6617 . . . . . 6 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴onto𝐵)
9 forn 6588 . . . . . 6 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
108, 9syl 17 . . . . 5 (𝑓:𝐴1-1-onto𝐵 → ran 𝑓 = 𝐵)
114rnex 7611 . . . . 5 ran 𝑓 ∈ V
1210, 11eqeltrrdi 2922 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐵 ∈ V)
137, 12jca 514 . . 3 (𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
1413exlimiv 1927 . 2 (∃𝑓 𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15 f1oeq2 6600 . . . 4 (𝑥 = 𝐴 → (𝑓:𝑥1-1-onto𝑦𝑓:𝐴1-1-onto𝑦))
1615exbidv 1918 . . 3 (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑦))
17 f1oeq3 6601 . . . 4 (𝑦 = 𝐵 → (𝑓:𝐴1-1-onto𝑦𝑓:𝐴1-1-onto𝐵))
1817exbidv 1918 . . 3 (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
19 df-en 8504 . . 3 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
2016, 18, 19brabg 5419 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
211, 14, 20pm5.21nii 382 1 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398   = wceq 1533  wex 1776  wcel 2110  Vcvv 3495   class class class wbr 5059  dom cdm 5550  ran crn 5551   Fn wfn 6345  ontowfo 6348  1-1-ontowf1o 6349  cen 8500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322  ax-un 7455
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-xp 5556  df-rel 5557  df-cnv 5558  df-dm 5560  df-rn 5561  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-en 8504
This theorem is referenced by:  domen  8516  f1oen3g  8519  ener  8550  en0  8566  ensn1  8567  en1  8570  unen  8590  enfixsn  8620  canth2  8664  mapen  8675  ssenen  8685  phplem4  8693  php3  8697  isinf  8725  ssfi  8732  domunfican  8785  fiint  8789  mapfien2  8866  unxpwdom2  9046  isinffi  9415  infxpenc2  9442  fseqen  9447  dfac8b  9451  infpwfien  9482  dfac12r  9566  infmap2  9634  cff1  9674  infpssr  9724  fin4en1  9725  enfin2i  9737  enfin1ai  9800  axcc3  9854  axcclem  9873  numth  9888  ttukey2g  9932  canthnum  10065  canthwe  10067  canthp1  10070  pwfseq  10080  tskuni  10199  gruen  10228  hasheqf1o  13703  hashfacen  13806  fz1f1o  15061  ruc  15590  cnso  15594  eulerth  16114  ablfaclem3  19203  lbslcic  20979  uvcendim  20985  indishmph  22400  ufldom  22564  ovolctb  24085  ovoliunlem3  24099  iunmbl2  24152  dyadmbl  24195  vitali  24208  cusgrfilem3  27233  padct  30449  f1ocnt  30519  volmeas  31485  eulerpart  31635  derangenlem  32413  mblfinlem1  34923  eldioph2lem1  39350  isnumbasgrplem1  39694  nnf1oxpnn  41449  sprsymrelen  43655  prproropen  43663  uspgrspren  44020  uspgrbisymrel  44022  rrx2xpreen  44699
  Copyright terms: Public domain W3C validator