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

Theorem fvelimad 6958
Description: Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
fvelimad.x 𝑥𝐹
fvelimad.f (𝜑𝐹 Fn 𝐴)
fvelimad.c (𝜑𝐶 ∈ (𝐹𝐵))
Assertion
Ref Expression
fvelimad (𝜑 → ∃𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐹(𝑥)

Proof of Theorem fvelimad
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fvelimad.c . . . 4 (𝜑𝐶 ∈ (𝐹𝐵))
2 elimag 6062 . . . . 5 (𝐶 ∈ (𝐹𝐵) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑦𝐵 𝑦𝐹𝐶))
32ibi 266 . . . 4 (𝐶 ∈ (𝐹𝐵) → ∃𝑦𝐵 𝑦𝐹𝐶)
41, 3syl 17 . . 3 (𝜑 → ∃𝑦𝐵 𝑦𝐹𝐶)
5 nfv 1915 . . . 4 𝑦𝜑
6 nfre1 3280 . . . 4 𝑦𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶
7 vex 3476 . . . . . . . . . . 11 𝑦 ∈ V
87a1i 11 . . . . . . . . . 10 ((𝜑𝑦𝐹𝐶) → 𝑦 ∈ V)
91adantr 479 . . . . . . . . . 10 ((𝜑𝑦𝐹𝐶) → 𝐶 ∈ (𝐹𝐵))
10 simpr 483 . . . . . . . . . 10 ((𝜑𝑦𝐹𝐶) → 𝑦𝐹𝐶)
118, 9, 10breldmd 5911 . . . . . . . . 9 ((𝜑𝑦𝐹𝐶) → 𝑦 ∈ dom 𝐹)
12 fvelimad.f . . . . . . . . . . 11 (𝜑𝐹 Fn 𝐴)
1312fndmd 6653 . . . . . . . . . 10 (𝜑 → dom 𝐹 = 𝐴)
1413adantr 479 . . . . . . . . 9 ((𝜑𝑦𝐹𝐶) → dom 𝐹 = 𝐴)
1511, 14eleqtrd 2833 . . . . . . . 8 ((𝜑𝑦𝐹𝐶) → 𝑦𝐴)
16153adant2 1129 . . . . . . 7 ((𝜑𝑦𝐵𝑦𝐹𝐶) → 𝑦𝐴)
17 simp2 1135 . . . . . . 7 ((𝜑𝑦𝐵𝑦𝐹𝐶) → 𝑦𝐵)
1816, 17elind 4193 . . . . . 6 ((𝜑𝑦𝐵𝑦𝐹𝐶) → 𝑦 ∈ (𝐴𝐵))
19 fnfun 6648 . . . . . . . . 9 (𝐹 Fn 𝐴 → Fun 𝐹)
2012, 19syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
21203ad2ant1 1131 . . . . . . 7 ((𝜑𝑦𝐵𝑦𝐹𝐶) → Fun 𝐹)
22 simp3 1136 . . . . . . 7 ((𝜑𝑦𝐵𝑦𝐹𝐶) → 𝑦𝐹𝐶)
23 funbrfv 6941 . . . . . . 7 (Fun 𝐹 → (𝑦𝐹𝐶 → (𝐹𝑦) = 𝐶))
2421, 22, 23sylc 65 . . . . . 6 ((𝜑𝑦𝐵𝑦𝐹𝐶) → (𝐹𝑦) = 𝐶)
25 rspe 3244 . . . . . 6 ((𝑦 ∈ (𝐴𝐵) ∧ (𝐹𝑦) = 𝐶) → ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶)
2618, 24, 25syl2anc 582 . . . . 5 ((𝜑𝑦𝐵𝑦𝐹𝐶) → ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶)
27263exp 1117 . . . 4 (𝜑 → (𝑦𝐵 → (𝑦𝐹𝐶 → ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶)))
285, 6, 27rexlimd 3261 . . 3 (𝜑 → (∃𝑦𝐵 𝑦𝐹𝐶 → ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶))
294, 28mpd 15 . 2 (𝜑 → ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶)
30 nfv 1915 . . 3 𝑦(𝐹𝑥) = 𝐶
31 fvelimad.x . . . . 5 𝑥𝐹
32 nfcv 2901 . . . . 5 𝑥𝑦
3331, 32nffv 6900 . . . 4 𝑥(𝐹𝑦)
3433nfeq1 2916 . . 3 𝑥(𝐹𝑦) = 𝐶
35 fveqeq2 6899 . . 3 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝐶 ↔ (𝐹𝑦) = 𝐶))
3630, 34, 35cbvrexw 3302 . 2 (∃𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = 𝐶 ↔ ∃𝑦 ∈ (𝐴𝐵)(𝐹𝑦) = 𝐶)
3729, 36sylibr 233 1 (𝜑 → ∃𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085   = wceq 1539  wcel 2104  wnfc 2881  wrex 3068  Vcvv 3472  cin 3946   class class class wbr 5147  dom cdm 5675  cima 5678  Fun wfun 6536   Fn wfn 6537  cfv 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550
This theorem is referenced by:  cyc3evpm  32579  cycpmgcl  32582  cycpmconjslem2  32584  cyc3conja  32586  limsupmnflem  44734  liminfvalxr  44797
  Copyright terms: Public domain W3C validator