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

Theorem dffo3 6335
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 6081 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 ffn 6007 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 fnrnfv 6204 . . . . . 6 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
43eqeq1d 2623 . . . . 5 (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
52, 4syl 17 . . . 4 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵))
6 simpr 477 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦 = (𝐹𝑥))
7 ffvelrn 6318 . . . . . . . . . . . 12 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
87adantr 481 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
96, 8eqeltrd 2698 . . . . . . . . . 10 (((𝐹:𝐴𝐵𝑥𝐴) ∧ 𝑦 = (𝐹𝑥)) → 𝑦𝐵)
109exp31 629 . . . . . . . . 9 (𝐹:𝐴𝐵 → (𝑥𝐴 → (𝑦 = (𝐹𝑥) → 𝑦𝐵)))
1110rexlimdv 3024 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵))
1211biantrurd 529 . . . . . . 7 (𝐹:𝐴𝐵 → ((𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))))
13 dfbi2 659 . . . . . . 7 ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ((∃𝑥𝐴 𝑦 = (𝐹𝑥) → 𝑦𝐵) ∧ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1412, 13syl6rbbr 279 . . . . . 6 (𝐹:𝐴𝐵 → ((∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ (𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
1514albidv 1846 . . . . 5 (𝐹:𝐴𝐵 → (∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥))))
16 abeq1 2730 . . . . 5 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ 𝑦𝐵))
17 df-ral 2912 . . . . 5 (∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∀𝑦(𝑦𝐵 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
1815, 16, 173bitr4g 303 . . . 4 (𝐹:𝐴𝐵 → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
195, 18bitrd 268 . . 3 (𝐹:𝐴𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
2019pm5.32i 668 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
211, 20bitri 264 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  ran crn 5080   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852
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 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
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 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  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-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fo 5858  df-fv 5860
This theorem is referenced by:  dffo4  6336  foelrn  6339  foco2  6340  foco2OLD  6341  fcofo  6503  foov  6768  resixpfo  7897  fofinf1o  8192  wdom2d  8436  brwdom3  8438  isf32lem9  9134  hsmexlem2  9200  cnref1o  11778  wwlktovfo  13642  1arith  15562  fullestrcsetc  16719  fullsetcestrc  16734  orbsta  17674  symgextfo  17770  symgfixfo  17787  pwssplit1  18987  znf1o  19828  cygznlem3  19846  scmatfo  20264  m2cpmfo  20489  pm2mpfo  20547  recosf1o  24198  efif1olem4  24208  dvdsmulf1o  24833  wlkpwwlkf1ouspgr  26647  wlknwwlksnsur  26658  wlkwwlksur  26665  wwlksnextsur  26677  clwwlksfo  26797  clwlksfoclwwlk  26842  eucrctshift  26982  frgrncvvdeqlemC  27049  numclwlk1lem2fo  27096  subfacp1lem3  30899  cvmfolem  30996  finixpnum  33053  wessf1ornlem  38868  projf1o  38883  sumnnodd  39289  dvnprodlem1  39489  fourierdlem54  39705  nnfoctbdjlem  40000  isomenndlem  40072  sprsymrelfo  41056  uspgrsprfo  41065
  Copyright terms: Public domain W3C validator