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

Theorem bren 7909
 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 7908 . 2 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2 f1ofn 6097 . . . . 5 (𝑓:𝐴1-1-onto𝐵𝑓 Fn 𝐴)
3 fndm 5950 . . . . . 6 (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4 vex 3194 . . . . . . 7 𝑓 ∈ V
54dmex 7047 . . . . . 6 dom 𝑓 ∈ V
63, 5syl6eqelr 2713 . . . . 5 (𝑓 Fn 𝐴𝐴 ∈ V)
72, 6syl 17 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐴 ∈ V)
8 f1ofo 6103 . . . . . 6 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴onto𝐵)
9 forn 6077 . . . . . 6 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
108, 9syl 17 . . . . 5 (𝑓:𝐴1-1-onto𝐵 → ran 𝑓 = 𝐵)
114rnex 7048 . . . . 5 ran 𝑓 ∈ V
1210, 11syl6eqelr 2713 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐵 ∈ V)
137, 12jca 554 . . 3 (𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
1413exlimiv 1860 . 2 (∃𝑓 𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15 f1oeq2 6087 . . . 4 (𝑥 = 𝐴 → (𝑓:𝑥1-1-onto𝑦𝑓:𝐴1-1-onto𝑦))
1615exbidv 1852 . . 3 (𝑥 = 𝐴 → (∃𝑓 𝑓:𝑥1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑦))
17 f1oeq3 6088 . . . 4 (𝑦 = 𝐵 → (𝑓:𝐴1-1-onto𝑦𝑓:𝐴1-1-onto𝐵))
1817exbidv 1852 . . 3 (𝑦 = 𝐵 → (∃𝑓 𝑓:𝐴1-1-onto𝑦 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
19 df-en 7901 . . 3 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
2016, 18, 19brabg 4959 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
211, 14, 20pm5.21nii 368 1 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1992  Vcvv 3191   class class class wbr 4618  dom cdm 5079  ran crn 5080   Fn wfn 5845  –onto→wfo 5848  –1-1-onto→wf1o 5849   ≈ cen 7897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-xp 5085  df-rel 5086  df-cnv 5087  df-dm 5089  df-rn 5090  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-en 7901 This theorem is referenced by:  domen  7913  f1oen3g  7916  ener  7947  enerOLD  7948  en0  7964  ensn1  7965  en1  7968  unen  7985  enfixsn  8014  canth2  8058  mapen  8069  ssenen  8079  phplem4  8087  php3  8091  isinf  8118  ssfi  8125  domunfican  8178  fiint  8182  mapfien2  8259  unxpwdom2  8438  isinffi  8763  infxpenc2  8790  fseqen  8795  dfac8b  8799  infpwfien  8830  dfac12r  8913  infmap2  8985  cff1  9025  infpssr  9075  fin4en1  9076  enfin2i  9088  enfin1ai  9151  axcc3  9205  axcclem  9224  numth  9239  ttukey2g  9283  canthnum  9416  canthwe  9418  canthp1  9421  pwfseq  9431  tskuni  9550  gruen  9579  hasheqf1o  13074  hashfacen  13173  fz1f1o  14369  ruc  14892  cnso  14896  eulerth  15407  ablfaclem3  18402  lbslcic  20094  uvcendim  20100  indishmph  21506  ufldom  21671  ovolctb  23160  ovoliunlem3  23174  iunmbl2  23227  dyadmbl  23269  vitali  23283  cusgrfilem3  26234  wlknwwlksnen  26642  padct  29331  f1ocnt  29392  volmeas  30067  eulerpart  30217  derangenlem  30853  mblfinlem1  33064  eldioph2lem1  36789  isnumbasgrplem1  37138  nnf1oxpnn  38844
 Copyright terms: Public domain W3C validator