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

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

Proof of Theorem fnres
StepHypRef Expression
1 ancom 450 . . 3 ((∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
2 vex 3394 . . . . . . . . . 10 𝑦 ∈ V
32brres 5606 . . . . . . . . 9 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐹𝑦𝑥𝐴))
4 ancom 450 . . . . . . . . 9 ((𝑥𝐹𝑦𝑥𝐴) ↔ (𝑥𝐴𝑥𝐹𝑦))
53, 4bitri 266 . . . . . . . 8 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦))
65mobii 2655 . . . . . . 7 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∃*𝑦(𝑥𝐴𝑥𝐹𝑦))
7 moanimv 2695 . . . . . . 7 (∃*𝑦(𝑥𝐴𝑥𝐹𝑦) ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
86, 7bitri 266 . . . . . 6 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
98albii 1904 . . . . 5 (∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
10 relres 5629 . . . . . 6 Rel (𝐹𝐴)
11 dffun6 6116 . . . . . 6 (Fun (𝐹𝐴) ↔ (Rel (𝐹𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦))
1210, 11mpbiran 691 . . . . 5 (Fun (𝐹𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦)
13 df-ral 3101 . . . . 5 (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
149, 12, 133bitr4i 294 . . . 4 (Fun (𝐹𝐴) ↔ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦)
15 dmres 5622 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
16 inss1 4029 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
1715, 16eqsstri 3832 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
18 eqss 3813 . . . . . 6 (dom (𝐹𝐴) = 𝐴 ↔ (dom (𝐹𝐴) ⊆ 𝐴𝐴 ⊆ dom (𝐹𝐴)))
1917, 18mpbiran 691 . . . . 5 (dom (𝐹𝐴) = 𝐴𝐴 ⊆ dom (𝐹𝐴))
20 dfss3 3787 . . . . . 6 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴))
2115elin2 4000 . . . . . . . . 9 (𝑥 ∈ dom (𝐹𝐴) ↔ (𝑥𝐴𝑥 ∈ dom 𝐹))
2221baib 527 . . . . . . . 8 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ 𝑥 ∈ dom 𝐹))
23 vex 3394 . . . . . . . . 9 𝑥 ∈ V
2423eldm 5522 . . . . . . . 8 (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦)
2522, 24syl6bb 278 . . . . . . 7 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ ∃𝑦 𝑥𝐹𝑦))
2625ralbiia 3167 . . . . . 6 (∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2720, 26bitri 266 . . . . 5 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2819, 27bitri 266 . . . 4 (dom (𝐹𝐴) = 𝐴 ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2914, 28anbi12i 614 . . 3 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦))
30 r19.26 3252 . . 3 (∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
311, 29, 303bitr4i 294 . 2 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
32 df-fn 6104 . 2 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
33 eu5 2658 . . 3 (∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3433ralbii 3168 . 2 (∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3531, 32, 343bitr4i 294 1 ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2156  ∃!weu 2630  ∃*wmo 2631  wral 3096  cin 3768  wss 3769   class class class wbr 4844  dom cdm 5311  cres 5313  Rel wrel 5316  Fun wfun 6095   Fn wfn 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-res 5323  df-fun 6103  df-fn 6104
This theorem is referenced by:  f1ompt  6603  omxpenlem  8300  tz6.12-afv  41762  tz6.12-afv2  41829
  Copyright terms: Public domain W3C validator