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

Theorem dff13 5510
Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.)
Assertion
Ref Expression
dff13 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem dff13
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 dff12 5180 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2 ffn 5128 . . . 4 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 vex 2618 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4 vex 2618 . . . . . . . . . . . . . . 15 𝑧 ∈ V
53, 4breldm 4610 . . . . . . . . . . . . . 14 (𝑥𝐹𝑧𝑥 ∈ dom 𝐹)
6 fndm 5080 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76eleq2d 2154 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹𝑥𝐴))
85, 7syl5ib 152 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑥𝐹𝑧𝑥𝐴))
9 vex 2618 . . . . . . . . . . . . . . 15 𝑦 ∈ V
109, 4breldm 4610 . . . . . . . . . . . . . 14 (𝑦𝐹𝑧𝑦 ∈ dom 𝐹)
116eleq2d 2154 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1210, 11syl5ib 152 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑦𝐹𝑧𝑦𝐴))
138, 12anim12d 328 . . . . . . . . . . . 12 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) → (𝑥𝐴𝑦𝐴)))
1413pm4.71rd 386 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
15 eqcom 2087 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑧)
16 fnbrfvb 5310 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑧𝑥𝐹𝑧))
1715, 16syl5bb 190 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑧 = (𝐹𝑥) ↔ 𝑥𝐹𝑧))
18 eqcom 2087 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑦) ↔ (𝐹𝑦) = 𝑧)
19 fnbrfvb 5310 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑦𝐴) → ((𝐹𝑦) = 𝑧𝑦𝐹𝑧))
2018, 19syl5bb 190 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑦𝐴) → (𝑧 = (𝐹𝑦) ↔ 𝑦𝐹𝑧))
2117, 20bi2anan9 571 . . . . . . . . . . . . 13 (((𝐹 Fn 𝐴𝑥𝐴) ∧ (𝐹 Fn 𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2221anandis 557 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2322pm5.32da 440 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
2414, 23bitr4d 189 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))))
2524imbi1d 229 . . . . . . . . 9 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦)))
26 impexp 259 . . . . . . . . 9 ((((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
2725, 26syl6bb 194 . . . . . . . 8 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
2827albidv 1749 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
29 19.21v 1798 . . . . . . . 8 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
30 funfvex 5287 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ V)
3130funfni 5081 . . . . . . . . . . . . 13 ((𝐹 Fn 𝐴𝑥𝐴) → (𝐹𝑥) ∈ V)
32 eqvincg 2732 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ V → ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))))
3331, 32syl 14 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))))
3433imbi1d 229 . . . . . . . . . . 11 ((𝐹 Fn 𝐴𝑥𝐴) → (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
35 19.23v 1808 . . . . . . . . . . 11 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
3634, 35syl6rbbr 197 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝑥𝐴) → (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3736adantrr 463 . . . . . . . . 9 ((𝐹 Fn 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3837pm5.74da 432 . . . . . . . 8 (𝐹 Fn 𝐴 → (((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
3929, 38syl5bb 190 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
4028, 39bitrd 186 . . . . . 6 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
41402albidv 1792 . . . . 5 (𝐹 Fn 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
42 breq1 3825 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐹𝑧𝑦𝐹𝑧))
4342mo4 2006 . . . . . . 7 (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4443albii 1402 . . . . . 6 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
45 alrot3 1417 . . . . . 6 (∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4644, 45bitri 182 . . . . 5 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
47 r2al 2393 . . . . 5 (∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4841, 46, 473bitr4g 221 . . . 4 (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
492, 48syl 14 . . 3 (𝐹:𝐴𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
5049pm5.32i 442 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
511, 50bitri 182 1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1285   = wceq 1287  wex 1424  wcel 1436  ∃*wmo 1946  wral 2355  Vcvv 2615   class class class wbr 3822  dom cdm 4413   Fn wfn 4978  wf 4979  1-1wf1 4980  cfv 4983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-sbc 2830  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fv 4991
This theorem is referenced by:  f1veqaeq  5511  dff13f  5512  dff1o6  5518  fcof1  5525  f1o2ndf1  5952  cnref1o  9068  frec2uzf1od  9744  iseqf1olemqf1o  9830  crth  11106  peano4nninf  11365  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator