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

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

Proof of Theorem fnres
StepHypRef Expression
1 ancom 266 . . 3 ((∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
2 vex 2741 . . . . . . . . . 10 𝑦 ∈ V
32brres 4914 . . . . . . . . 9 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐹𝑦𝑥𝐴))
4 ancom 266 . . . . . . . . 9 ((𝑥𝐹𝑦𝑥𝐴) ↔ (𝑥𝐴𝑥𝐹𝑦))
53, 4bitri 184 . . . . . . . 8 (𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦))
65mobii 2063 . . . . . . 7 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∃*𝑦(𝑥𝐴𝑥𝐹𝑦))
7 moanimv 2101 . . . . . . 7 (∃*𝑦(𝑥𝐴𝑥𝐹𝑦) ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
86, 7bitri 184 . . . . . 6 (∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ (𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
98albii 1470 . . . . 5 (∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
10 relres 4936 . . . . . 6 Rel (𝐹𝐴)
11 dffun6 5231 . . . . . 6 (Fun (𝐹𝐴) ↔ (Rel (𝐹𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦))
1210, 11mpbiran 940 . . . . 5 (Fun (𝐹𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹𝐴)𝑦)
13 df-ral 2460 . . . . 5 (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑥𝐹𝑦))
149, 12, 133bitr4i 212 . . . 4 (Fun (𝐹𝐴) ↔ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦)
15 dmres 4929 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
16 inss1 3356 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
1715, 16eqsstri 3188 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
18 eqss 3171 . . . . . 6 (dom (𝐹𝐴) = 𝐴 ↔ (dom (𝐹𝐴) ⊆ 𝐴𝐴 ⊆ dom (𝐹𝐴)))
1917, 18mpbiran 940 . . . . 5 (dom (𝐹𝐴) = 𝐴𝐴 ⊆ dom (𝐹𝐴))
20 dfss3 3146 . . . . . 6 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴))
2115elin2 3324 . . . . . . . . 9 (𝑥 ∈ dom (𝐹𝐴) ↔ (𝑥𝐴𝑥 ∈ dom 𝐹))
2221baib 919 . . . . . . . 8 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ 𝑥 ∈ dom 𝐹))
23 vex 2741 . . . . . . . . 9 𝑥 ∈ V
2423eldm 4825 . . . . . . . 8 (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦)
2522, 24bitrdi 196 . . . . . . 7 (𝑥𝐴 → (𝑥 ∈ dom (𝐹𝐴) ↔ ∃𝑦 𝑥𝐹𝑦))
2625ralbiia 2491 . . . . . 6 (∀𝑥𝐴 𝑥 ∈ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2720, 26bitri 184 . . . . 5 (𝐴 ⊆ dom (𝐹𝐴) ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2819, 27bitri 184 . . . 4 (dom (𝐹𝐴) = 𝐴 ↔ ∀𝑥𝐴𝑦 𝑥𝐹𝑦)
2914, 28anbi12i 460 . . 3 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ (∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴𝑦 𝑥𝐹𝑦))
30 r19.26 2603 . . 3 (∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥𝐴𝑦 𝑥𝐹𝑦 ∧ ∀𝑥𝐴 ∃*𝑦 𝑥𝐹𝑦))
311, 29, 303bitr4i 212 . 2 ((Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴) ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
32 df-fn 5220 . 2 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
33 eu5 2073 . . 3 (∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3433ralbii 2483 . 2 (∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦))
3531, 32, 343bitr4i 212 1 ((𝐹𝐴) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑥𝐹𝑦)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wex 1492  ∃!weu 2026  ∃*wmo 2027  wcel 2148  wral 2455  cin 3129  wss 3130   class class class wbr 4004  dom cdm 4627  cres 4629  Rel wrel 4632  Fun wfun 5211   Fn wfn 5212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-opab 4066  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-res 4639  df-fun 5219  df-fn 5220
This theorem is referenced by:  f1ompt  5668
  Copyright terms: Public domain W3C validator