![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnfvima | Structured version Visualization version GIF version |
Description: The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.) |
Ref | Expression |
---|---|
fnfvima | ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 6638 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | 3ad2ant1 1133 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹) |
3 | simp2 1137 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴) | |
4 | fndm 6641 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
5 | 4 | 3ad2ant1 1133 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴) |
6 | 3, 5 | sseqtrrd 4019 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹) |
7 | 2, 6 | jca 512 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹)) |
8 | simp3 1138 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) | |
9 | funfvima2 7217 | . 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))) | |
10 | 7, 8, 9 | sylc 65 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ⊆ wss 3944 dom cdm 5669 “ cima 5672 Fun wfun 6526 Fn wfn 6527 ‘cfv 6532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6484 df-fun 6534 df-fn 6535 df-fv 6540 |
This theorem is referenced by: fnfvimad 7220 isomin 7318 isofrlem 7321 fnwelem 8099 fimaproj 8103 php3 9195 php3OLD 9207 fissuni 9340 unxpwdom2 9565 cantnflt 9649 dfac12lem2 10121 ackbij2 10220 isf34lem7 10356 isf34lem6 10357 zorn2lem2 10474 ttukeylem5 10490 tskuni 10760 axpre-sup 11146 limsupval2 15406 mhmima 18681 ghmnsgima 19082 psgnunilem1 19325 dprdfeq0 19851 dprd2dlem1 19870 lmhmima 20607 lmcnp 22737 basqtop 23144 tgqtop 23145 kqfvima 23163 reghmph 23226 uzrest 23330 qustgpopn 23553 qustgplem 23554 cphsqrtcl 24630 lhop 25462 ig1peu 25618 ig1pdvds 25623 plypf1 25655 nosupno 27133 nosupbday 27135 noinfno 27148 noinfbday 27150 noetasuplem4 27166 noetainflem4 27170 eqscut2 27233 scutun12 27237 scutbdaybnd 27242 scutbdaybnd2 27243 scutbdaylt 27245 madebdaylemlrcut 27316 cofcut1 27327 cofcutr 27331 lrrecfr 27343 negsproplem4 27421 negsproplem5 27422 negsproplem6 27423 f1otrg 27987 txomap 32645 sitgaddlemb 33178 f1resrcmplf1dlem 33920 cvmopnlem 34100 mrsubrn 34335 msubrn 34351 poimirlem4 36296 poimirlem6 36298 poimirlem7 36299 poimirlem16 36308 poimirlem17 36309 poimirlem19 36311 poimirlem20 36312 poimirlem23 36315 cnambfre 36340 ftc1anclem7 36371 ftc1anc 36373 isnumbasgrplem1 41614 funimaeq 43723 mgmhmima 46344 |
Copyright terms: Public domain | W3C validator |