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 6454 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | dfrel4v 6047 | . . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | sylib 220 | . . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) |
4 | fnbr 6459 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) | |
5 | 4 | ex 415 | . . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 565 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
7 | eqcom 2828 | . . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦) | |
8 | fnbrfvb 6718 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) | |
9 | 7, 8 | syl5bb 285 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
10 | 9 | pm5.32da 581 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
11 | 6, 10 | bitr4d 284 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)))) |
12 | 11 | opabbidv 5132 | . . . 4 ⊢ (𝐹 Fn 𝐴 → {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
13 | 3, 12 | eqtrd 2856 | . . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
14 | df-mpt 5147 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))} | |
15 | 13, 14 | syl6eqr 2874 | . 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
16 | fvex 6683 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
17 | eqid 2821 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) | |
18 | 16, 17 | fnmpti 6491 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴 |
19 | fneq1 6444 | . . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴)) | |
20 | 18, 19 | mpbiri 260 | . 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴) |
21 | 15, 20 | impbii 211 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 class class class wbr 5066 {copab 5128 ↦ cmpt 5146 Rel wrel 5560 Fn wfn 6350 ‘cfv 6355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-iota 6314 df-fun 6357 df-fn 6358 df-fv 6363 |
This theorem is referenced by: fnrnfv 6725 feqmptd 6733 dffn5f 6736 eqfnfv 6802 fndmin 6815 fcompt 6895 funiun 6909 resfunexg 6978 eufnfv 6991 nvocnv 7038 fnov 7282 offveqb 7431 caofinvl 7436 oprabco 7791 df1st2 7793 df2nd2 7794 curry1 7799 curry2 7802 resixpfo 8500 pw2f1olem 8621 marypha2lem3 8901 seqof 13428 prmrec 16258 prdsbascl 16756 xpsaddlem 16846 xpsvsca 16850 oppccatid 16989 fuclid 17236 fucrid 17237 curfuncf 17488 yonedainv 17531 yonffthlem 17532 prdsidlem 17943 pws0g 17947 prdsinvlem 18208 gsummptmhm 19060 staffn 19620 prdslmodd 19741 ofco2 21060 1mavmul 21157 cnmpt1st 22276 cnmpt2nd 22277 ptunhmeo 22416 xpsxmetlem 22989 xpsmet 22992 itg2split 24350 pserulm 25010 pserdvlem2 25016 logcn 25230 logblog 25370 emcllem5 25577 gamcvg2lem 25636 crctcshlem4 27598 eucrct2eupth 28024 fcomptf 30403 gsummpt2d 30687 pl1cn 31198 esumpcvgval 31337 esumcvgsum 31347 eulerpartgbij 31630 dstfrvclim1 31735 ptpconn 32480 knoppcnlem8 33839 knoppcnlem11 33842 ctbssinf 34690 curfv 34887 ovoliunnfl 34949 voliunnfl 34951 fnopabco 35013 upixp 35019 prdsbnd 35086 prdstotbnd 35087 prdsbnd2 35088 fgraphopab 39830 expgrowthi 40685 expgrowth 40687 uzmptshftfval 40698 dvcosre 42216 fourierdlem56 42467 fourierdlem62 42473 fundcmpsurbijinjpreimafv 43587 fundcmpsurinjimaid 43591 fdmdifeqresdif 44410 offvalfv 44411 |
Copyright terms: Public domain | W3C validator |