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

Theorem relelfvdm 5419
 Description: If a function value has a member, the argument belongs to the domain. (Contributed by Jim Kingdon, 22-Jan-2019.)
Assertion
Ref Expression
relelfvdm ((Rel 𝐹𝐴 ∈ (𝐹𝐵)) → 𝐵 ∈ dom 𝐹)

Proof of Theorem relelfvdm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfv 5385 . . . . . 6 (𝐴 ∈ (𝐹𝐵) ↔ ∃𝑥(𝐴𝑥 ∧ ∀𝑦(𝐵𝐹𝑦𝑦 = 𝑥)))
2 exsimpr 1580 . . . . . 6 (∃𝑥(𝐴𝑥 ∧ ∀𝑦(𝐵𝐹𝑦𝑦 = 𝑥)) → ∃𝑥𝑦(𝐵𝐹𝑦𝑦 = 𝑥))
31, 2sylbi 120 . . . . 5 (𝐴 ∈ (𝐹𝐵) → ∃𝑥𝑦(𝐵𝐹𝑦𝑦 = 𝑥))
4 equsb1 1741 . . . . . . . 8 [𝑥 / 𝑦]𝑦 = 𝑥
5 spsbbi 1798 . . . . . . . 8 (∀𝑦(𝐵𝐹𝑦𝑦 = 𝑥) → ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ [𝑥 / 𝑦]𝑦 = 𝑥))
64, 5mpbiri 167 . . . . . . 7 (∀𝑦(𝐵𝐹𝑦𝑦 = 𝑥) → [𝑥 / 𝑦]𝐵𝐹𝑦)
7 nfv 1491 . . . . . . . 8 𝑦 𝐵𝐹𝑥
8 breq2 3901 . . . . . . . 8 (𝑦 = 𝑥 → (𝐵𝐹𝑦𝐵𝐹𝑥))
97, 8sbie 1747 . . . . . . 7 ([𝑥 / 𝑦]𝐵𝐹𝑦𝐵𝐹𝑥)
106, 9sylib 121 . . . . . 6 (∀𝑦(𝐵𝐹𝑦𝑦 = 𝑥) → 𝐵𝐹𝑥)
1110eximi 1562 . . . . 5 (∃𝑥𝑦(𝐵𝐹𝑦𝑦 = 𝑥) → ∃𝑥 𝐵𝐹𝑥)
123, 11syl 14 . . . 4 (𝐴 ∈ (𝐹𝐵) → ∃𝑥 𝐵𝐹𝑥)
1312anim2i 337 . . 3 ((Rel 𝐹𝐴 ∈ (𝐹𝐵)) → (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
14 19.42v 1860 . . 3 (∃𝑥(Rel 𝐹𝐵𝐹𝑥) ↔ (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
1513, 14sylibr 133 . 2 ((Rel 𝐹𝐴 ∈ (𝐹𝐵)) → ∃𝑥(Rel 𝐹𝐵𝐹𝑥))
16 releldm 4742 . . 3 ((Rel 𝐹𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
1716exlimiv 1560 . 2 (∃𝑥(Rel 𝐹𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
1815, 17syl 14 1 ((Rel 𝐹𝐴 ∈ (𝐹𝐵)) → 𝐵 ∈ dom 𝐹)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1312  ∃wex 1451   ∈ wcel 1463  [wsb 1718   class class class wbr 3897  dom cdm 4507  Rel wrel 4512  ‘cfv 5091 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-xp 4513  df-rel 4514  df-dm 4517  df-iota 5056  df-fv 5099 This theorem is referenced by:  mptrcl  5469  elfvmptrab1  5481  elmpocl  5934  oprssdmm  6035  mpoxopn0yelv  6102  eluzel2  9280  hashinfom  10464  istopon  12075  istps  12094  topontopn  12099  eltg4i  12119  eltg3  12121  tg1  12123  tg2  12124  tgclb  12129  cldrcl  12166  neiss2  12206  lmrcl  12255  cnprcl2k  12270  metflem  12413  xmetf  12414  ismet2  12418  xmeteq0  12423  xmettri2  12425  xmetpsmet  12433  xmetres2  12443  blfvalps  12449  blex  12451  blvalps  12452  blval  12453  blfps  12473  blf  12474  mopnval  12506  isxms2  12516  comet  12563
 Copyright terms: Public domain W3C validator