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

Theorem dffo3 6414
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 6157 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 ffn 6083 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 fnrnfv 6281 . . . . . 6 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
43eqeq1d 2653 . . . . 5 (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
52, 4syl 17 . . . 4 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
6 simpr 476 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦 = (𝐹𝑥))
7 ffvelrn 6397 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
87adantr 480 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
96, 8eqeltrd 2730 . . . . . . . . . 10 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦𝐵)
109exp31 629 . . . . . . . . 9 (𝐹:𝐴𝐵 → (𝑥𝐴 → (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
1110rexlimdv 3059 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵))
1211biantrurd 528 . . . . . . 7 (𝐹:𝐴𝐵 → ((𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))))
13 dfbi2 661 . . . . . . 7 ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1412, 13syl6rbbr 279 . . . . . 6 (𝐹:𝐴𝐵 → ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1514albidv 1889 . . . . 5 (𝐹:𝐴𝐵 → (∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
16 abeq1 2762 . . . . 5 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵))
17 df-ral 2946 . . . . 5 (∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
1815, 16, 173bitr4g 303 . . . 4 (𝐹:𝐴𝐵 → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
195, 18bitrd 268 . . 3 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
2019pm5.32i 670 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
211, 20bitri 264 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  ran crn 5144   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fo 5932  df-fv 5934
This theorem is referenced by:  dffo4  6415  foelrn  6418  foco2  6419  foco2OLD  6420  fcofo  6583  foov  6850  resixpfo  7988  fofinf1o  8282  wdom2d  8526  brwdom3  8528  isf32lem9  9221  hsmexlem2  9287  cnref1o  11865  wwlktovfo  13747  1arith  15678  fullestrcsetc  16838  fullsetcestrc  16853  orbsta  17792  symgextfo  17888  symgfixfo  17905  pwssplit1  19107  znf1o  19948  cygznlem3  19966  scmatfo  20384  m2cpmfo  20609  pm2mpfo  20667  recosf1o  24326  efif1olem4  24336  dvdsmulf1o  24965  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnextsur  26863  clwwlkfo  27013  clwlksfoclwwlk  27050  eucrctshift  27221  frgrncvvdeqlem9  27287  numclwlk1lem2fo  27348  subfacp1lem3  31290  cvmfolem  31387  finixpnum  33524  wessf1ornlem  39685  projf1o  39700  sumnnodd  40180  dvnprodlem1  40479  fourierdlem54  40695  nnfoctbdjlem  40990  isomenndlem  41065  sprsymrelfo  42072  uspgrsprfo  42081
  Copyright terms: Public domain W3C validator