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

Theorem fnres 4941
 Description: An equivalence for functionality of a restriction. Compare dffun8 4855. (Contributed by Mario Carneiro, 20-May-2015.)
Assertion
Ref Expression
fnres ((𝐹A) Fn Ax A ∃!y x𝐹y)
Distinct variable groups:   x,y,A   x,𝐹,y

Proof of Theorem fnres
StepHypRef Expression
1 ancom 253 . . 3 ((x A ∃*y x𝐹y x A y x𝐹y) ↔ (x A y x𝐹y x A ∃*y x𝐹y))
2 vex 2538 . . . . . . . . . 10 y V
32brres 4545 . . . . . . . . 9 (x(𝐹A)y ↔ (x𝐹y x A))
4 ancom 253 . . . . . . . . 9 ((x𝐹y x A) ↔ (x A x𝐹y))
53, 4bitri 173 . . . . . . . 8 (x(𝐹A)y ↔ (x A x𝐹y))
65mobii 1919 . . . . . . 7 (∃*y x(𝐹A)y∃*y(x A x𝐹y))
7 moanimv 1957 . . . . . . 7 (∃*y(x A x𝐹y) ↔ (x A∃*y x𝐹y))
86, 7bitri 173 . . . . . 6 (∃*y x(𝐹A)y ↔ (x A∃*y x𝐹y))
98albii 1339 . . . . 5 (x∃*y x(𝐹A)yx(x A∃*y x𝐹y))
10 relres 4566 . . . . . 6 Rel (𝐹A)
11 dffun6 4842 . . . . . 6 (Fun (𝐹A) ↔ (Rel (𝐹A) x∃*y x(𝐹A)y))
1210, 11mpbiran 835 . . . . 5 (Fun (𝐹A) ↔ x∃*y x(𝐹A)y)
13 df-ral 2289 . . . . 5 (x A ∃*y x𝐹yx(x A∃*y x𝐹y))
149, 12, 133bitr4i 201 . . . 4 (Fun (𝐹A) ↔ x A ∃*y x𝐹y)
15 dmres 4559 . . . . . . 7 dom (𝐹A) = (A ∩ dom 𝐹)
16 inss1 3134 . . . . . . 7 (A ∩ dom 𝐹) ⊆ A
1715, 16eqsstri 2952 . . . . . 6 dom (𝐹A) ⊆ A
18 eqss 2937 . . . . . 6 (dom (𝐹A) = A ↔ (dom (𝐹A) ⊆ A A ⊆ dom (𝐹A)))
1917, 18mpbiran 835 . . . . 5 (dom (𝐹A) = AA ⊆ dom (𝐹A))
20 dfss3 2912 . . . . . 6 (A ⊆ dom (𝐹A) ↔ x A x dom (𝐹A))
2115elin2 3104 . . . . . . . . 9 (x dom (𝐹A) ↔ (x A x dom 𝐹))
2221baib 818 . . . . . . . 8 (x A → (x dom (𝐹A) ↔ x dom 𝐹))
23 vex 2538 . . . . . . . . 9 x V
2423eldm 4459 . . . . . . . 8 (x dom 𝐹y x𝐹y)
2522, 24syl6bb 185 . . . . . . 7 (x A → (x dom (𝐹A) ↔ y x𝐹y))
2625ralbiia 2316 . . . . . 6 (x A x dom (𝐹A) ↔ x A y x𝐹y)
2720, 26bitri 173 . . . . 5 (A ⊆ dom (𝐹A) ↔ x A y x𝐹y)
2819, 27bitri 173 . . . 4 (dom (𝐹A) = Ax A y x𝐹y)
2914, 28anbi12i 436 . . 3 ((Fun (𝐹A) dom (𝐹A) = A) ↔ (x A ∃*y x𝐹y x A y x𝐹y))
30 r19.26 2419 . . 3 (x A (y x𝐹y ∃*y x𝐹y) ↔ (x A y x𝐹y x A ∃*y x𝐹y))
311, 29, 303bitr4i 201 . 2 ((Fun (𝐹A) dom (𝐹A) = A) ↔ x A (y x𝐹y ∃*y x𝐹y))
32 df-fn 4832 . 2 ((𝐹A) Fn A ↔ (Fun (𝐹A) dom (𝐹A) = A))
33 eu5 1929 . . 3 (∃!y x𝐹y ↔ (y x𝐹y ∃*y x𝐹y))
3433ralbii 2308 . 2 (x A ∃!y x𝐹yx A (y x𝐹y ∃*y x𝐹y))
3531, 32, 343bitr4i 201 1 ((𝐹A) Fn Ax A ∃!y x𝐹y)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1226   = wceq 1228  ∃wex 1362   ∈ wcel 1374  ∃!weu 1882  ∃*wmo 1883  ∀wral 2284   ∩ cin 2893   ⊆ wss 2894   class class class wbr 3738  dom cdm 4272   ↾ cres 4274  Rel wrel 4277  Fun wfun 4823   Fn wfn 4824 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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918 This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-v 2537  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-br 3739  df-opab 3793  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-res 4284  df-fun 4831  df-fn 4832 This theorem is referenced by:  f1ompt  5245
 Copyright terms: Public domain W3C validator