![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffn5 | Structured version Visualization version GIF version |
Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
dffn5 | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 6316 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | dfrel4v 5915 | . . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | sylib 219 | . . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) |
4 | fnbr 6321 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) | |
5 | 4 | ex 413 | . . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 563 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
7 | eqcom 2800 | . . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦) | |
8 | fnbrfvb 6578 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) | |
9 | 7, 8 | syl5bb 284 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
10 | 9 | pm5.32da 579 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
11 | 6, 10 | bitr4d 283 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)))) |
12 | 11 | opabbidv 5022 | . . . 4 ⊢ (𝐹 Fn 𝐴 → {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
13 | 3, 12 | eqtrd 2829 | . . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
14 | df-mpt 5036 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))} | |
15 | 13, 14 | syl6eqr 2847 | . 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
16 | fvex 6543 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
17 | eqid 2793 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) | |
18 | 16, 17 | fnmpti 6351 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴 |
19 | fneq1 6306 | . . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴)) | |
20 | 18, 19 | mpbiri 259 | . 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴) |
21 | 15, 20 | impbii 210 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1520 ∈ wcel 2079 class class class wbr 4956 {copab 5018 ↦ cmpt 5035 Rel wrel 5440 Fn wfn 6212 ‘cfv 6217 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pr 5214 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-sbc 3702 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-iota 6181 df-fun 6219 df-fn 6220 df-fv 6225 |
This theorem is referenced by: fnrnfv 6585 feqmptd 6593 dffn5f 6596 eqfnfv 6658 fndmin 6671 fcompt 6749 funiun 6763 resfunexg 6835 eufnfv 6848 nvocnv 6894 fnov 7129 offveqb 7280 caofinvl 7285 oprabco 7638 df1st2 7640 df2nd2 7641 curry1 7646 curry2 7649 resixpfo 8338 pw2f1olem 8458 marypha2lem3 8737 seqof 13265 prmrec 16075 prdsbascl 16573 xpsaddlem 16663 xpsvsca 16667 oppccatid 16806 fuclid 17053 fucrid 17054 curfuncf 17305 yonedainv 17348 yonffthlem 17349 prdsidlem 17749 pws0g 17753 prdsinvlem 17953 gsummptmhm 18768 staffn 19298 prdslmodd 19419 ofco2 20732 1mavmul 20829 cnmpt1st 21948 cnmpt2nd 21949 ptunhmeo 22088 xpsxmetlem 22660 xpsmet 22663 itg2split 24021 pserulm 24681 pserdvlem2 24687 logcn 24899 logblog 25039 emcllem5 25247 gamcvg2lem 25306 crctcshlem4 27273 eucrct2eupthOLD 27701 eucrct2eupth 27702 fcomptf 30066 gsummpt2d 30454 pl1cn 30771 esumpcvgval 30910 esumcvgsum 30920 eulerpartgbij 31203 dstfrvclim1 31308 ptpconn 32044 knoppcnlem8 33392 knoppcnlem11 33395 ctbssinf 34164 curfv 34349 ovoliunnfl 34411 voliunnfl 34413 fnopabco 34476 upixp 34482 prdsbnd 34549 prdstotbnd 34550 prdsbnd2 34551 fgraphopab 39246 expgrowthi 40155 expgrowth 40157 uzmptshftfval 40168 dvcosre 41691 fourierdlem56 41943 fourierdlem62 41949 fdmdifeqresdif 43822 offvalfv 43823 |
Copyright terms: Public domain | W3C validator |