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

Theorem bren 8118
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 8117 . 2 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2 f1ofn 6279 . . . . 5 (𝑓:𝐴1-1-onto𝐵𝑓 Fn 𝐴)
3 fndm 6130 . . . . . 6 (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4 vex 3354 . . . . . . 7 𝑓 ∈ V
54dmex 7246 . . . . . 6 dom 𝑓 ∈ V
63, 5syl6eqelr 2859 . . . . 5 (𝑓 Fn 𝐴𝐴 ∈ V)
72, 6syl 17 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐴 ∈ V)
8 f1ofo 6285 . . . . . 6 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴onto𝐵)
9 forn 6259 . . . . . 6 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
108, 9syl 17 . . . . 5 (𝑓:𝐴1-1-onto𝐵 → ran 𝑓 = 𝐵)
114rnex 7247 . . . . 5 ran 𝑓 ∈ V
1210, 11syl6eqelr 2859 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐵 ∈ V)
137, 12jca 501 . . 3 (𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
1413exlimiv 2010 . 2 (∃𝑓 𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15 f1oeq2 6269 . . . 4 (𝑥 = 𝐴 → (𝑓:𝑥1-1-onto𝑦𝑓:𝐴1-1-onto𝑦))
1615exbidv 2002 . . 3 (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑦))
17 f1oeq3 6270 . . . 4 (𝑦 = 𝐵 → (𝑓:𝐴1-1-onto𝑦𝑓:𝐴1-1-onto𝐵))
1817exbidv 2002 . . 3 (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
19 df-en 8110 . . 3 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
2016, 18, 19brabg 5127 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
211, 14, 20pm5.21nii 367 1 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  Vcvv 3351   class class class wbr 4786  dom cdm 5249  ran crn 5250   Fn wfn 6026  ontowfo 6029  1-1-ontowf1o 6030  cen 8106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-rel 5256  df-cnv 5257  df-dm 5259  df-rn 5260  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-en 8110
This theorem is referenced by:  domen  8122  f1oen3g  8125  ener  8156  en0  8172  ensn1  8173  en1  8176  unen  8196  enfixsn  8225  canth2  8269  mapen  8280  ssenen  8290  phplem4  8298  php3  8302  isinf  8329  ssfi  8336  domunfican  8389  fiint  8393  mapfien2  8470  unxpwdom2  8649  isinffi  9018  infxpenc2  9045  fseqen  9050  dfac8b  9054  infpwfien  9085  dfac12r  9170  infmap2  9242  cff1  9282  infpssr  9332  fin4en1  9333  enfin2i  9345  enfin1ai  9408  axcc3  9462  axcclem  9481  numth  9496  ttukey2g  9540  canthnum  9673  canthwe  9675  canthp1  9678  pwfseq  9688  tskuni  9807  gruen  9836  hasheqf1o  13341  hashfacen  13440  fz1f1o  14649  ruc  15178  cnso  15182  eulerth  15695  ablfaclem3  18694  lbslcic  20397  uvcendim  20403  indishmph  21822  ufldom  21986  ovolctb  23478  ovoliunlem3  23492  iunmbl2  23545  dyadmbl  23588  vitali  23601  cusgrfilem3  26588  padct  29837  f1ocnt  29899  volmeas  30634  eulerpart  30784  derangenlem  31491  mblfinlem1  33779  eldioph2lem1  37849  isnumbasgrplem1  38197  nnf1oxpnn  39904  sprsymrelen  42278  uspgrspren  42288  uspgrbisymrel  42290
  Copyright terms: Public domain W3C validator