![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvelimab | Structured version Visualization version GIF version |
Description: Function value in an image. (Contributed by NM, 20-Jan-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by David Abernethy, 17-Dec-2011.) |
Ref | Expression |
---|---|
fvelimab | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3433 | . . 3 ⊢ (𝐶 ∈ (𝐹 “ 𝐵) → 𝐶 ∈ V) | |
2 | 1 | anim2i 607 | . 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ (𝐹 “ 𝐵)) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V)) |
3 | fvex 6514 | . . . . 5 ⊢ (𝐹‘𝑥) ∈ V | |
4 | eleq1 2853 | . . . . 5 ⊢ ((𝐹‘𝑥) = 𝐶 → ((𝐹‘𝑥) ∈ V ↔ 𝐶 ∈ V)) | |
5 | 3, 4 | mpbii 225 | . . . 4 ⊢ ((𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V) |
6 | 5 | rexlimivw 3227 | . . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V) |
7 | 6 | anim2i 607 | . 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V)) |
8 | eleq1 2853 | . . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ (𝐹 “ 𝐵) ↔ 𝐶 ∈ (𝐹 “ 𝐵))) | |
9 | eqeq2 2789 | . . . . . . 7 ⊢ (𝑦 = 𝐶 → ((𝐹‘𝑥) = 𝑦 ↔ (𝐹‘𝑥) = 𝐶)) | |
10 | 9 | rexbidv 3242 | . . . . . 6 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
11 | 8, 10 | bibi12d 338 | . . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦) ↔ (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))) |
12 | 11 | imbi2d 333 | . . . 4 ⊢ (𝑦 = 𝐶 → (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)))) |
13 | fnfun 6288 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
14 | fndm 6290 | . . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
15 | 14 | sseq2d 3891 | . . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴)) |
16 | 15 | biimpar 470 | . . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ dom 𝐹) |
17 | dfimafn 6560 | . . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦}) | |
18 | 13, 16, 17 | syl2an2r 672 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦}) |
19 | 18 | abeq2d 2899 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦)) |
20 | 12, 19 | vtoclg 3486 | . . 3 ⊢ (𝐶 ∈ V → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))) |
21 | 20 | impcom 399 | . 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
22 | 2, 7, 21 | pm5.21nd 789 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 {cab 2758 ∃wrex 3089 Vcvv 3415 ⊆ wss 3831 dom cdm 5408 “ cima 5411 Fun wfun 6184 Fn wfn 6185 ‘cfv 6190 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-fv 6198 |
This theorem is referenced by: fvelimabd 6569 ssimaex 6578 rexima 6826 ralima 6827 f1elima 6848 ovelimab 7144 tcrank 9109 djuun 9151 ackbij2 9465 fin1a2lem6 9627 iunfo 9761 grothomex 10051 axpre-sup 10391 injresinjlem 12975 txkgen 21967 fmucndlem 22606 efopn 24945 pjimai 29737 fimarab 30155 fimaproj 30741 qtophaus 30744 indf1ofs 30929 eulerpartgbij 31275 eulerpartlemgvv 31279 ballotlemsima 31419 elmthm 32343 elintfv 32527 nocvxmin 32769 isnacs2 38698 isnacs3 38702 islmodfg 39065 kercvrlsm 39079 isnumbasgrplem2 39100 dfacbasgrp 39104 unima 40847 fourierdlem62 41885 |
Copyright terms: Public domain | W3C validator |