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

Theorem dffo3 6517
Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
Assertion
Ref Expression
dffo3 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦

Proof of Theorem dffo3
StepHypRef Expression
1 dffo2 6260 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 ffn 6185 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 fnrnfv 6384 . . . . . 6 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
43eqeq1d 2773 . . . . 5 (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
52, 4syl 17 . . . 4 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
6 simpr 471 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦 = (𝐹𝑥))
7 ffvelrn 6500 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
87adantr 466 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
96, 8eqeltrd 2850 . . . . . . . . . 10 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦𝐵)
109exp31 406 . . . . . . . . 9 (𝐹:𝐴𝐵 → (𝑥𝐴 → (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
1110rexlimdv 3178 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵))
1211biantrurd 516 . . . . . . 7 (𝐹:𝐴𝐵 → ((𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))))
13 dfbi2 460 . . . . . . 7 ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1412, 13syl6rbbr 279 . . . . . 6 (𝐹:𝐴𝐵 → ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1514albidv 2001 . . . . 5 (𝐹:𝐴𝐵 → (∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
16 abeq1 2882 . . . . 5 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵))
17 df-ral 3066 . . . . 5 (∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
1815, 16, 173bitr4g 303 . . . 4 (𝐹:𝐴𝐵 → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
195, 18bitrd 268 . . 3 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
2019pm5.32i 556 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
211, 20bitri 264 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1629   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wrex 3062  ran crn 5250   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031
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-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
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  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-sbc 3588  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-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fo 6037  df-fv 6039
This theorem is referenced by:  dffo4  6518  foelrn  6521  foco2  6522  fcofo  6686  foov  6955  resixpfo  8100  fofinf1o  8397  wdom2d  8641  brwdom3  8643  isf32lem9  9385  hsmexlem2  9451  cnref1o  12030  wwlktovfo  13911  1arith  15838  fullestrcsetc  16999  fullsetcestrc  17014  orbsta  17953  symgextfo  18049  symgfixfo  18066  pwssplit1  19272  znf1o  20115  cygznlem3  20133  scmatfo  20554  m2cpmfo  20781  pm2mpfo  20839  recosf1o  24502  efif1olem4  24512  dvdsmulf1o  25141  wlkswwlksf1o  27013  wlknwwlksnsurOLD  27024  wlkwwlksurOLD  27032  wwlksnextsur  27044  clwlkclwwlkfo  27159  clwwlkfo  27206  clwlksfoclwwlkOLD  27244  eucrctshift  27423  frgrncvvdeqlem9  27489  numclwwlk1lem2fo  27544  subfacp1lem3  31502  cvmfolem  31599  finixpnum  33727  wessf1ornlem  39891  projf1o  39906  sumnnodd  40380  dvnprodlem1  40679  fourierdlem54  40894  nnfoctbdjlem  41189  isomenndlem  41264  sprsymrelfo  42275  uspgrsprfo  42284
  Copyright terms: Public domain W3C validator