Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dffn5im | GIF version |
Description: Representation of a function in terms of its values. The converse holds given the law of the excluded middle; as it is we have most of the converse via funmpt 5220 and dmmptss 5094. (Contributed by Jim Kingdon, 31-Dec-2018.) |
Ref | Expression |
---|---|
dffn5im | ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 5280 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | dfrel4v 5049 | . . . 4 ⊢ (Rel 𝐹 ↔ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | sylib 121 | . . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) |
4 | fnbr 5284 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) | |
5 | 4 | ex 114 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 392 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
7 | eqcom 2166 | . . . . . . 7 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦) | |
8 | fnbrfvb 5521 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) | |
9 | 7, 8 | syl5bb 191 | . . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
10 | 9 | pm5.32da 448 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
11 | 6, 10 | bitr4d 190 | . . . 4 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)))) |
12 | 11 | opabbidv 4042 | . . 3 ⊢ (𝐹 Fn 𝐴 → {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
13 | 3, 12 | eqtrd 2197 | . 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
14 | df-mpt 4039 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))} | |
15 | 13, 14 | eqtr4di 2215 | 1 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1342 ∈ wcel 2135 class class class wbr 3976 {copab 4036 ↦ cmpt 4037 Rel wrel 4603 Fn wfn 5177 ‘cfv 5182 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-14 2138 ax-ext 2146 ax-sep 4094 ax-pow 4147 ax-pr 4181 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-v 2723 df-sbc 2947 df-un 3115 df-in 3117 df-ss 3124 df-pw 3555 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-opab 4038 df-mpt 4039 df-id 4265 df-xp 4604 df-rel 4605 df-cnv 4606 df-co 4607 df-dm 4608 df-iota 5147 df-fun 5184 df-fn 5185 df-fv 5190 |
This theorem is referenced by: fnrnfv 5527 feqmptd 5533 dffn5imf 5535 eqfnfv 5577 fndmin 5586 fcompt 5649 resfunexg 5700 eufnfv 5709 fnovim 5941 offveqb 6063 caofinvl 6066 oprabco 6176 df1st2 6178 df2nd2 6179 xpen 6802 cnmpt1st 12835 cnmpt2nd 12836 |
Copyright terms: Public domain | W3C validator |