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

Theorem f1oen2g 8322
Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8324 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
f1oen2g ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Proof of Theorem f1oen2g
StepHypRef Expression
1 f1of 6442 . . . 4 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 fex2 7452 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
31, 2syl3an1 1144 . . 3 ((𝐹:𝐴1-1-onto𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
433coml 1108 . 2 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐹 ∈ V)
5 simp3 1119 . 2 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐹:𝐴1-1-onto𝐵)
6 f1oen3g 8321 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
74, 5, 6syl2anc 576 1 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1069  wcel 2051  Vcvv 3410   class class class wbr 4926  wf 6182  1-1-ontowf1o 6185  cen 8302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-en 8306
This theorem is referenced by:  f1oeng  8324  enrefg  8337  en2d  8341  en3d  8342  ener  8352  f1imaen2g  8366  cnven  8381  xpcomen  8403  omxpen  8414  pw2eng  8418  unfilem3  8578  xpfi  8583  hsmexlem1  9645  iccen  12698  uzenom  13146  nnenom  13162  eqgen  18129  dfod2  18465  hmphen  22113  clwlkclwwlken  27542  clwlkclwwlkenOLD  27543  clwwlken  27590  clwwlkenOLD  27591  clwwlknonclwlknonen  27928  clwwlknonclwlknonenOLD  27929  dlwwlknondlwlknonen  27934  dlwwlknondlwlknonenOLD  27935
  Copyright terms: Public domain W3C validator