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 6542 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | 3ad2ant1 1132 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹) |
3 | simp2 1136 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴) | |
4 | fndm 6545 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
5 | 4 | 3ad2ant1 1132 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴) |
6 | 3, 5 | sseqtrrd 3963 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹) |
7 | 2, 6 | jca 512 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹)) |
8 | simp3 1137 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) | |
9 | funfvima2 7116 | . 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))) | |
10 | 7, 8, 9 | sylc 65 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ⊆ wss 3888 dom cdm 5590 “ cima 5593 Fun wfun 6431 Fn wfn 6432 ‘cfv 6437 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-opab 5138 df-id 5490 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-iota 6395 df-fun 6439 df-fn 6440 df-fv 6445 |
This theorem is referenced by: fnfvimad 7119 isomin 7217 isofrlem 7220 fnwelem 7981 fimaproj 7985 php3 9004 php3OLD 9016 fissuni 9133 unxpwdom2 9356 cantnflt 9439 dfac12lem2 9909 ackbij2 10008 isf34lem7 10144 isf34lem6 10145 zorn2lem2 10262 ttukeylem5 10278 tskuni 10548 axpre-sup 10934 limsupval2 15198 mhmima 18472 ghmnsgima 18867 psgnunilem1 19110 dprdfeq0 19634 dprd2dlem1 19653 lmhmima 20318 lmcnp 22464 basqtop 22871 tgqtop 22872 kqfvima 22890 reghmph 22953 uzrest 23057 qustgpopn 23280 qustgplem 23281 cphsqrtcl 24357 lhop 25189 ig1peu 25345 ig1pdvds 25350 plypf1 25382 f1otrg 27241 txomap 31793 sitgaddlemb 32324 f1resrcmplf1dlem 33067 cvmopnlem 33249 mrsubrn 33484 msubrn 33500 nosupno 33915 nosupbday 33917 noinfno 33930 noinfbday 33932 noetasuplem4 33948 noetainflem4 33952 eqscut2 34009 scutun12 34013 scutbdaybnd 34018 scutbdaybnd2 34019 scutbdaylt 34021 madebdaylemlrcut 34088 cofcut1 34099 cofcutr 34101 lrrecfr 34109 poimirlem4 35790 poimirlem6 35792 poimirlem7 35793 poimirlem16 35802 poimirlem17 35803 poimirlem19 35805 poimirlem20 35806 poimirlem23 35809 cnambfre 35834 ftc1anclem7 35865 ftc1anc 35867 isnumbasgrplem1 40933 funimaeq 42799 mgmhmima 45367 |
Copyright terms: Public domain | W3C validator |