ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dffo4 GIF version

Theorem dffo4 5486
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 5272 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
2 simpl 108 . . . 4 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
3 vex 2636 . . . . . . . . . 10 𝑦 ∈ V
43elrn 4710 . . . . . . . . 9 (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 𝑥𝐹𝑦)
5 eleq2 2158 . . . . . . . . 9 (ran 𝐹 = 𝐵 → (𝑦 ∈ ran 𝐹𝑦𝐵))
64, 5syl5bbr 193 . . . . . . . 8 (ran 𝐹 = 𝐵 → (∃𝑥 𝑥𝐹𝑦𝑦𝐵))
76biimpar 292 . . . . . . 7 ((ran 𝐹 = 𝐵𝑦𝐵) → ∃𝑥 𝑥𝐹𝑦)
87adantll 461 . . . . . 6 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → ∃𝑥 𝑥𝐹𝑦)
9 ffn 5195 . . . . . . . . . . 11 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
10 fnbr 5150 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
1110ex 114 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
129, 11syl 14 . . . . . . . . . 10 (𝐹:𝐴𝐵 → (𝑥𝐹𝑦𝑥𝐴))
1312ancrd 320 . . . . . . . . 9 (𝐹:𝐴𝐵 → (𝑥𝐹𝑦 → (𝑥𝐴𝑥𝐹𝑦)))
1413eximdv 1815 . . . . . . . 8 (𝐹:𝐴𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥(𝑥𝐴𝑥𝐹𝑦)))
15 df-rex 2376 . . . . . . . 8 (∃𝑥𝐴 𝑥𝐹𝑦 ↔ ∃𝑥(𝑥𝐴𝑥𝐹𝑦))
1614, 15syl6ibr 161 . . . . . . 7 (𝐹:𝐴𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑥𝐹𝑦))
1716ad2antrr 473 . . . . . 6 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑥𝐹𝑦))
188, 17mpd 13 . . . . 5 (((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦𝐵) → ∃𝑥𝐴 𝑥𝐹𝑦)
1918ralrimiva 2458 . . . 4 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦)
202, 19jca 301 . . 3 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
211, 20sylbi 120 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
22 fnbrfvb 5380 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
2322biimprd 157 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑥𝐹𝑦 → (𝐹𝑥) = 𝑦))
24 eqcom 2097 . . . . . . . 8 ((𝐹𝑥) = 𝑦𝑦 = (𝐹𝑥))
2523, 24syl6ib 160 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑥𝐹𝑦𝑦 = (𝐹𝑥)))
269, 25sylan 278 . . . . . 6 ((𝐹:𝐴𝐵𝑥𝐴) → (𝑥𝐹𝑦𝑦 = (𝐹𝑥)))
2726reximdva 2487 . . . . 5 (𝐹:𝐴𝐵 → (∃𝑥𝐴 𝑥𝐹𝑦 → ∃𝑥𝐴 𝑦 = (𝐹𝑥)))
2827ralimdv 2454 . . . 4 (𝐹:𝐴𝐵 → (∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦 → ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
2928imdistani 435 . . 3 ((𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦) → (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
30 dffo3 5485 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑦 = (𝐹𝑥)))
3129, 30sylibr 133 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦) → 𝐹:𝐴onto𝐵)
3221, 31impbii 125 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵𝑥𝐴 𝑥𝐹𝑦))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1296  wex 1433  wcel 1445  wral 2370  wrex 2371   class class class wbr 3867  ran crn 4468   Fn wfn 5044  wf 5045  ontowfo 5047  cfv 5049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-sbc 2855  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-opab 3922  df-mpt 3923  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-fo 5055  df-fv 5057
This theorem is referenced by:  dffo5  5487
  Copyright terms: Public domain W3C validator