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

Theorem dffo3 6866
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 6593 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 ffn 6513 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 fnrnfv 6724 . . . . . 6 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
43eqeq1d 2828 . . . . 5 (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
52, 4syl 17 . . . 4 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
6 simpr 485 . . . . . . . . . 10 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦 = (𝐹𝑥))
7 ffvelrn 6847 . . . . . . . . . . 11 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
87adantr 481 . . . . . . . . . 10 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
96, 8eqeltrd 2918 . . . . . . . . 9 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦𝐵)
109rexlimdva2 3292 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵))
1110biantrurd 533 . . . . . . 7 (𝐹:𝐴𝐵 → ((𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))))
12 dfbi2 475 . . . . . . 7 ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1311, 12syl6rbbr 291 . . . . . 6 (𝐹:𝐴𝐵 → ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1413albidv 1914 . . . . 5 (𝐹:𝐴𝐵 → (∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
15 abeq1 2951 . . . . 5 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵))
16 df-ral 3148 . . . . 5 (∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
1714, 15, 163bitr4g 315 . . . 4 (𝐹:𝐴𝐵 → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
185, 17bitrd 280 . . 3 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
1918pm5.32i 575 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
201, 19bitri 276 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1528   = wceq 1530  wcel 2107  {cab 2804  wral 3143  wrex 3144  ran crn 5555   Fn wfn 6349  wf 6350  ontowfo 6352  cfv 6354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-fo 6360  df-fv 6362
This theorem is referenced by:  dffo4  6867  foelrn  6870  foco2  6871  fcofo  7040  foov  7316  resixpfo  8494  fofinf1o  8793  wdom2d  9038  brwdom3  9040  isf32lem9  9777  hsmexlem2  9843  cnref1o  12379  wwlktovfo  14317  1arith  16258  fullestrcsetc  17396  fullsetcestrc  17411  orbsta  18388  symgextfo  18486  symgfixfo  18503  pwssplit1  19767  znf1o  20633  cygznlem3  20651  scmatfo  21074  m2cpmfo  21299  pm2mpfo  21357  recosf1o  25051  efif1olem4  25061  dvdsmulf1o  25704  wlkswwlksf1o  27590  wwlksnextsurj  27611  clwlkclwwlkfo  27720  clwwlkfo  27762  eucrctshift  27955  frgrncvvdeqlem9  28019  numclwwlk1lem2fo  28070  subfacp1lem3  32332  cvmfolem  32429  finixpnum  34763  wessf1ornlem  41329  projf1o  41343  sumnnodd  41795  dvnprodlem1  42115  fourierdlem54  42330  nnfoctbdjlem  42622  isomenndlem  42697  sprsymrelfo  43510  prproropf1o  43520  isomuspgrlem2d  43847  uspgrsprfo  43874  rrx2xpref1o  44607
  Copyright terms: Public domain W3C validator