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 6448 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | dfrel4v 6041 | . . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | sylib 220 | . . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) |
4 | fnbr 6453 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) | |
5 | 4 | ex 415 | . . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 565 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
7 | eqcom 2828 | . . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦) | |
8 | fnbrfvb 6712 | . . . . . . . 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 5124 | . . . 4 ⊢ (𝐹 Fn 𝐴 → {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
13 | 3, 12 | eqtrd 2856 | . . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
14 | df-mpt 5139 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))} | |
15 | 13, 14 | syl6eqr 2874 | . 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
16 | fvex 6677 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
17 | eqid 2821 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) | |
18 | 16, 17 | fnmpti 6485 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴 |
19 | fneq1 6438 | . . 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 1533 ∈ wcel 2110 class class class wbr 5058 {copab 5120 ↦ cmpt 5138 Rel wrel 5554 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 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 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 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fn 6352 df-fv 6357 |
This theorem is referenced by: fnrnfv 6719 feqmptd 6727 dffn5f 6730 eqfnfv 6796 fndmin 6809 fcompt 6889 funiun 6903 resfunexg 6972 eufnfv 6985 nvocnv 7032 fnov 7276 offveqb 7425 caofinvl 7430 oprabco 7785 df1st2 7787 df2nd2 7788 curry1 7793 curry2 7796 resixpfo 8494 pw2f1olem 8615 marypha2lem3 8895 seqof 13421 prmrec 16252 prdsbascl 16750 xpsaddlem 16840 xpsvsca 16844 oppccatid 16983 fuclid 17230 fucrid 17231 curfuncf 17482 yonedainv 17525 yonffthlem 17526 prdsidlem 17937 pws0g 17941 prdsinvlem 18202 gsummptmhm 19054 staffn 19614 prdslmodd 19735 ofco2 21054 1mavmul 21151 cnmpt1st 22270 cnmpt2nd 22271 ptunhmeo 22410 xpsxmetlem 22983 xpsmet 22986 itg2split 24344 pserulm 25004 pserdvlem2 25010 logcn 25224 logblog 25364 emcllem5 25571 gamcvg2lem 25630 crctcshlem4 27592 eucrct2eupth 28018 fcomptf 30397 gsummpt2d 30682 pl1cn 31193 esumpcvgval 31332 esumcvgsum 31342 eulerpartgbij 31625 dstfrvclim1 31730 ptpconn 32475 knoppcnlem8 33834 knoppcnlem11 33837 ctbssinf 34681 curfv 34866 ovoliunnfl 34928 voliunnfl 34930 fnopabco 34992 upixp 34998 prdsbnd 35065 prdstotbnd 35066 prdsbnd2 35067 fgraphopab 39803 expgrowthi 40658 expgrowth 40660 uzmptshftfval 40671 dvcosre 42189 fourierdlem56 42441 fourierdlem62 42447 fundcmpsurbijinjpreimafv 43561 fundcmpsurinjimaid 43565 fdmdifeqresdif 44384 offvalfv 44385 |
Copyright terms: Public domain | W3C validator |