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

Theorem dffo4 6415
Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
Assertion
Ref Expression
dffo4 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦

Proof of Theorem dffo4
StepHypRef Expression
1 dffo2 6157 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 simpl 472 . . . 4 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
3 vex 3234 . . . . . . . . . 10 𝑦 ∈ V
43elrn 5398 . . . . . . . . 9 (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 𝑥𝐹𝑦)
5 eleq2 2719 . . . . . . . . 9 (ran 𝐹 = 𝐵 → (𝑦 ∈ ran 𝐹𝑦𝐵))
64, 5syl5bbr 274 . . . . . . . 8 (ran 𝐹 = 𝐵 → (∃𝑥 𝑥𝐹𝑦𝑦𝐵))
76biimpar 501 . . . . . . 7 ((ran 𝐹 = 𝐵𝑦𝐵) → ∃𝑥 𝑥𝐹𝑦)
87adantll 750 . . . . . 6 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → ∃𝑥 𝑥𝐹𝑦)
9 ffn 6083 . . . . . . . . . . 11 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
10 fnbr 6031 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
1110ex 449 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
129, 11syl 17 . . . . . . . . . 10 (𝐹:𝐴𝐵 → (𝑥𝐹𝑦𝑥𝐴))
1312ancrd 576 . . . . . . . . 9 (𝐹:𝐴𝐵 → (𝑥𝐹𝑦 → (𝑥𝐴𝑥𝐹𝑦)))
1413eximdv 1886 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥(𝑥𝐴𝑥𝐹𝑦)))
15 df-rex 2947 . . . . . . . 8 (∃𝑥𝐴 𝑥𝐹𝑦 ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
1614, 15syl6ibr 242 . . . . . . 7 (𝐹:𝐴𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑥𝐹𝑦))
1716ad2antrr 762 . . . . . 6 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑥𝐹𝑦))
188, 17mpd 15 . . . . 5 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → ∃𝑥𝐴 𝑥𝐹𝑦)
1918ralrimiva 2995 . . . 4 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦)
202, 19jca 553 . . 3 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
211, 20sylbi 207 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
22 fnbrfvb 6274 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
2322biimprd 238 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑥𝐹𝑦 → (𝐹𝑥) = 𝑦))
24 eqcom 2658 . . . . . . . 8 ((𝐹𝑥) = 𝑦𝑦 = (𝐹𝑥))
2523, 24syl6ib 241 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑥𝐹𝑦𝑦 = (𝐹𝑥)))
269, 25sylan 487 . . . . . 6 ((𝐹:𝐴𝐵𝑥𝐴) → (𝑥𝐹𝑦𝑦 = (𝐹𝑥)))
2726reximdva 3046 . . . . 5 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
2827ralimdv 2992 . . . 4 (𝐹:𝐴𝐵 → (∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦 → ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
2928imdistani 726 . . 3 ((𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦) → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
30 dffo3 6414 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
3129, 30sylibr 224 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦) → 𝐹:𝐴onto𝐵)
3221, 31impbii 199 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942   class class class wbr 4685  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:  dffo5  6416  exfo  6417  brdom3  9388  phpreu  33523  poimirlem26  33565
  Copyright terms: Public domain W3C validator