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

Theorem funfvima 6373
Description: A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.)
Assertion
Ref Expression
funfvima ((Fun 𝐹𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))

Proof of Theorem funfvima
StepHypRef Expression
1 dmres 5325 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
21elin2 3762 . . . . . 6 (𝐵 ∈ dom (𝐹𝐴) ↔ (𝐵𝐴𝐵 ∈ dom 𝐹))
3 funres 5828 . . . . . . . . 9 (Fun 𝐹 → Fun (𝐹𝐴))
4 fvelrn 6244 . . . . . . . . 9 ((Fun (𝐹𝐴) ∧ 𝐵 ∈ dom (𝐹𝐴)) → ((𝐹𝐴)‘𝐵) ∈ ran (𝐹𝐴))
53, 4sylan 486 . . . . . . . 8 ((Fun 𝐹𝐵 ∈ dom (𝐹𝐴)) → ((𝐹𝐴)‘𝐵) ∈ ran (𝐹𝐴))
6 fvres 6101 . . . . . . . . . 10 (𝐵𝐴 → ((𝐹𝐴)‘𝐵) = (𝐹𝐵))
76eleq1d 2671 . . . . . . . . 9 (𝐵𝐴 → (((𝐹𝐴)‘𝐵) ∈ ran (𝐹𝐴) ↔ (𝐹𝐵) ∈ ran (𝐹𝐴)))
8 df-ima 5040 . . . . . . . . . 10 (𝐹𝐴) = ran (𝐹𝐴)
98eleq2i 2679 . . . . . . . . 9 ((𝐹𝐵) ∈ (𝐹𝐴) ↔ (𝐹𝐵) ∈ ran (𝐹𝐴))
107, 9syl6rbbr 277 . . . . . . . 8 (𝐵𝐴 → ((𝐹𝐵) ∈ (𝐹𝐴) ↔ ((𝐹𝐴)‘𝐵) ∈ ran (𝐹𝐴)))
115, 10syl5ibrcom 235 . . . . . . 7 ((Fun 𝐹𝐵 ∈ dom (𝐹𝐴)) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))
1211ex 448 . . . . . 6 (Fun 𝐹 → (𝐵 ∈ dom (𝐹𝐴) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
132, 12syl5bir 231 . . . . 5 (Fun 𝐹 → ((𝐵𝐴𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
1413expd 450 . . . 4 (Fun 𝐹 → (𝐵𝐴 → (𝐵 ∈ dom 𝐹 → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))))
1514com12 32 . . 3 (𝐵𝐴 → (Fun 𝐹 → (𝐵 ∈ dom 𝐹 → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))))
1615impd 445 . 2 (𝐵𝐴 → ((Fun 𝐹𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
1716pm2.43b 52 1 ((Fun 𝐹𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  dom cdm 5027  ran crn 5028  cres 5029  cima 5030  Fun wfun 5783  cfv 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-fv 5797
This theorem is referenced by:  funfvima2  6374  elovimad  6568  tz7.48-2  7401  tz9.12lem3  8512  lindff1  19925  txcnp  21180  c1liplem1  23507  htthlem  26951  tpr2rico  29079  brsiga  29366  erdszelem8  30227  nobndlem2  30885  nofulllem3  30896  relowlpssretop  32171  pthdivtx  40916
  Copyright terms: Public domain W3C validator