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

Theorem fnres 5015
Description: An equivalence for functionality of a restriction. Compare dffun8 4929. (Contributed by Mario Carneiro, 20-May-2015.)
Assertion
Ref Expression
fnres ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦

Proof of Theorem fnres
StepHypRef Expression
1 ancom 253 . . 3 ((∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
2 vex 2560 . . . . . . . . . 10 𝑦 ∈ V
32brres 4618 . . . . . . . . 9 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐹𝑦𝑥𝐴))
4 ancom 253 . . . . . . . . 9 ((𝑥𝐹𝑦𝑥𝐴) ↔ (𝑥𝐴𝑥𝐹𝑦))
53, 4bitri 173 . . . . . . . 8 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦))
65mobii 1937 . . . . . . 7 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∃*𝑦(𝑥𝐴𝑥𝐹𝑦))
7 moanimv 1975 . . . . . . 7 (∃*𝑦(𝑥𝐴𝑥𝐹𝑦) ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
86, 7bitri 173 . . . . . 6 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
98albii 1359 . . . . 5 (∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
10 relres 4639 . . . . . 6 Rel (𝐹𝐴)
11 dffun6 4916 . . . . . 6 (Fun (𝐹𝐴) ↔ (Rel (𝐹𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦))
1210, 11mpbiran 847 . . . . 5 (Fun (𝐹𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦)
13 df-ral 2311 . . . . 5 (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
149, 12, 133bitr4i 201 . . . 4 (Fun (𝐹𝐴) ↔ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦)
15 dmres 4632 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
16 inss1 3157 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
1715, 16eqsstri 2975 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
18 eqss 2960 . . . . . 6 (dom (𝐹𝐴) = 𝐴 ↔ (dom (𝐹𝐴) ⊆ 𝐴𝐴 ⊆ dom (𝐹𝐴)))
1917, 18mpbiran 847 . . . . 5 (dom (𝐹𝐴) = 𝐴𝐴 ⊆ dom (𝐹𝐴))
20 dfss3 2935 . . . . . 6 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴))
2115elin2 3127 . . . . . . . . 9 (𝑥 ∈ dom (𝐹𝐴) ↔ (𝑥𝐴𝑥 ∈ dom 𝐹))
2221baib 828 . . . . . . . 8 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ 𝑥 ∈ dom 𝐹))
23 vex 2560 . . . . . . . . 9 𝑥 ∈ V
2423eldm 4532 . . . . . . . 8 (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦)
2522, 24syl6bb 185 . . . . . . 7 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ ∃𝑦 𝑥𝐹𝑦))
2625ralbiia 2338 . . . . . 6 (∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2720, 26bitri 173 . . . . 5 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2819, 27bitri 173 . . . 4 (dom (𝐹𝐴) = 𝐴 ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2914, 28anbi12i 433 . . 3 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦))
30 r19.26 2441 . . 3 (∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
311, 29, 303bitr4i 201 . 2 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
32 df-fn 4905 . 2 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
33 eu5 1947 . . 3 (∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3433ralbii 2330 . 2 (∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3531, 32, 343bitr4i 201 1 ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98  wal 1241   = wceq 1243  wex 1381  wcel 1393  ∃!weu 1900  ∃*wmo 1901  wral 2306  cin 2916  wss 2917   class class class wbr 3764  dom cdm 4345  cres 4347  Rel wrel 4350  Fun wfun 4896   Fn wfn 4897
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765  df-opab 3819  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-res 4357  df-fun 4904  df-fn 4905
This theorem is referenced by:  f1ompt  5320
  Copyright terms: Public domain W3C validator