Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elpreima | Structured version Visualization version GIF version |
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
elpreima | ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvimass 5943 | . . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹 | |
2 | 1 | sseli 3962 | . . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹) |
3 | fndm 6449 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
4 | 3 | eleq2d 2898 | . . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴)) |
5 | 2, 4 | syl5ib 245 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴)) |
6 | fnfun 6447 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
7 | fvimacnvi 6815 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶) | |
8 | 6, 7 | sylan 580 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶) |
9 | 8 | ex 413 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶)) |
10 | 5, 9 | jcad 513 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
11 | fvimacnv 6816 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶))) | |
12 | 11 | funfni 6451 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶))) |
13 | 12 | biimpd 230 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶))) |
14 | 13 | expimpd 454 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶))) |
15 | 10, 14 | impbid 213 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 ◡ccnv 5548 dom cdm 5549 “ cima 5552 Fun wfun 6343 Fn wfn 6344 ‘cfv 6349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-fv 6357 |
This theorem is referenced by: elpreimad 6822 fniniseg 6823 fncnvima2 6824 unpreima 6826 respreima 6829 fnse 7818 brwitnlem 8123 unxpwdom2 9041 smobeth 9997 fpwwe2lem6 10046 fpwwe2lem9 10049 hashkf 13682 isercolllem2 15012 isercolllem3 15013 isercoll 15014 fsumss 15072 fprodss 15292 tanval 15471 1arith 16253 0ram 16346 ghmpreima 18320 ghmnsgpreima 18323 torsubg 18905 kerf1ghm 19428 kerf1hrmOLD 19429 lmhmpreima 19751 mpfind 20250 znunithash 20641 cncnpi 21816 cncnp 21818 cnpdis 21831 cnt0 21884 cnhaus 21892 2ndcomap 21996 1stccnp 22000 ptpjpre1 22109 tx1cn 22147 tx2cn 22148 txcnmpt 22162 txdis1cn 22173 hauseqlcld 22184 xkoptsub 22192 xkococn 22198 kqsat 22269 kqcldsat 22271 kqreglem1 22279 kqreglem2 22280 reghmph 22331 ordthmeolem 22339 tmdcn2 22627 clssubg 22646 tgphaus 22654 qustgplem 22658 ucncn 22823 xmeterval 22971 imasf1obl 23027 blval2 23101 metuel2 23104 isnghm 23261 cnbl0 23311 cnblcld 23312 cnheiborlem 23487 nmhmcn 23653 ismbl 24056 mbfeqalem1 24171 mbfmulc2lem 24177 mbfmax 24179 mbfposr 24182 mbfimaopnlem 24185 mbfaddlem 24190 mbfsup 24194 i1f1lem 24219 i1fpos 24236 mbfi1fseqlem4 24248 itg2monolem1 24280 itg2gt0 24290 itg2cnlem1 24291 itg2cnlem2 24292 plyeq0lem 24729 dgrlem 24748 dgrub 24753 dgrlb 24755 pserulm 24939 psercnlem2 24941 psercnlem1 24942 psercn 24943 abelth 24958 eff1olem 25059 ellogrn 25070 dvloglem 25158 logf1o2 25160 efopnlem1 25166 efopnlem2 25167 logtayl 25170 cxpcn3lem 25255 cxpcn3 25256 resqrtcn 25257 asinneg 25391 areambl 25464 sqff1o 25687 ubthlem1 28575 unipreima 30320 1stpreima 30369 2ndpreima 30370 suppss3 30387 hashgt1 30457 tocyc01 30688 cyc3evpm 30720 kerunit 30824 smatrcl 30961 cnre2csqlem 31053 elzrhunit 31120 qqhval2lem 31122 qqhf 31127 1stmbfm 31418 2ndmbfm 31419 mbfmcnt 31426 eulerpartlemsv2 31516 eulerpartlemv 31522 eulerpartlemf 31528 eulerpartlemgvv 31534 eulerpartlemgh 31536 eulerpartlemgs2 31538 sseqmw 31549 sseqf 31550 sseqp1 31553 fiblem 31556 fibp1 31559 cvmseu 32421 cvmliftmolem1 32426 cvmliftmolem2 32427 cvmliftlem15 32443 cvmlift2lem10 32457 cvmlift3lem8 32471 elmthm 32721 mthmblem 32725 mclsppslem 32728 mclspps 32729 cnambfre 34822 dvtan 34824 ftc1anclem3 34851 ftc1anclem5 34853 areacirc 34869 sstotbnd2 34935 keridl 35193 ellkr 36107 pw2f1ocnv 39514 binomcxplemdvbinom 40565 binomcxplemcvg 40566 binomcxplemnotnn0 40568 rfcnpre1 41156 rfcnpre2 41168 rfcnpre3 41170 rfcnpre4 41171 limsupresxr 41927 liminfresxr 41928 icccncfext 42050 sge0fodjrnlem 42579 smfsuplem1 42966 |
Copyright terms: Public domain | W3C validator |