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

Theorem fnres 6454
Description: An equivalence for functionality of a restriction. Compare dffun8 6362. (Contributed by Mario Carneiro, 20-May-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
Assertion
Ref Expression
fnres ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦

Proof of Theorem fnres
StepHypRef Expression
1 ancom 464 . . 3 ((∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
2 vex 3472 . . . . . . . . 9 𝑦 ∈ V
32brresi 5840 . . . . . . . 8 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦))
43mobii 2630 . . . . . . 7 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∃*𝑦(𝑥𝐴𝑥𝐹𝑦))
5 moanimv 2705 . . . . . . 7 (∃*𝑦(𝑥𝐴𝑥𝐹𝑦) ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
64, 5bitri 278 . . . . . 6 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
76albii 1821 . . . . 5 (∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
8 relres 5860 . . . . . 6 Rel (𝐹𝐴)
9 dffun6 6349 . . . . . 6 (Fun (𝐹𝐴) ↔ (Rel (𝐹𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦))
108, 9mpbiran 708 . . . . 5 (Fun (𝐹𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦)
11 df-ral 3135 . . . . 5 (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
127, 10, 113bitr4i 306 . . . 4 (Fun (𝐹𝐴) ↔ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦)
13 dmres 5853 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
14 inss1 4179 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
1513, 14eqsstri 3976 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
16 eqss 3957 . . . . . 6 (dom (𝐹𝐴) = 𝐴 ↔ (dom (𝐹𝐴) ⊆ 𝐴𝐴 ⊆ dom (𝐹𝐴)))
1715, 16mpbiran 708 . . . . 5 (dom (𝐹𝐴) = 𝐴𝐴 ⊆ dom (𝐹𝐴))
18 dfss3 3930 . . . . . 6 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴))
1913elin2 4148 . . . . . . . . 9 (𝑥 ∈ dom (𝐹𝐴) ↔ (𝑥𝐴𝑥 ∈ dom 𝐹))
2019baib 539 . . . . . . . 8 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ 𝑥 ∈ dom 𝐹))
21 vex 3472 . . . . . . . . 9 𝑥 ∈ V
2221eldm 5746 . . . . . . . 8 (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦)
2320, 22syl6bb 290 . . . . . . 7 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ ∃𝑦 𝑥𝐹𝑦))
2423ralbiia 3156 . . . . . 6 (∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2518, 24bitri 278 . . . . 5 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2617, 25bitri 278 . . . 4 (dom (𝐹𝐴) = 𝐴 ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2712, 26anbi12i 629 . . 3 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦))
28 r19.26 3162 . . 3 (∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
291, 27, 283bitr4i 306 . 2 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
30 df-fn 6337 . 2 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
31 df-eu 2653 . . 3 (∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3231ralbii 3157 . 2 (∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3329, 30, 323bitr4i 306 1 ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wex 1781  wcel 2114  ∃*wmo 2620  ∃!weu 2652  wral 3130  cin 3907  wss 3908   class class class wbr 5042  dom cdm 5532  cres 5534  Rel wrel 5537  Fun wfun 6328   Fn wfn 6329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-res 5544  df-fun 6336  df-fn 6337
This theorem is referenced by:  f1ompt  6857  omxpenlem  8605  tz6.12-afv  43668  tz6.12-afv2  43735
  Copyright terms: Public domain W3C validator