Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-map | GIF version |
Description: Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑𝑚 𝐵) (see mapval 6636). Many authors write 𝐴 followed by 𝐵 as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show 𝐵 as a prefixed superscript, which is read "𝐴 pre 𝐵 " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(𝐵, 𝐴) for our (𝐴 ↑𝑚 𝐵). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.) |
Ref | Expression |
---|---|
df-map | ⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmap 6624 | . 2 class ↑𝑚 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cvv 2730 | . . 3 class V | |
5 | 3 | cv 1347 | . . . . 5 class 𝑦 |
6 | 2 | cv 1347 | . . . . 5 class 𝑥 |
7 | vf | . . . . . 6 setvar 𝑓 | |
8 | 7 | cv 1347 | . . . . 5 class 𝑓 |
9 | 5, 6, 8 | wf 5192 | . . . 4 wff 𝑓:𝑦⟶𝑥 |
10 | 9, 7 | cab 2156 | . . 3 class {𝑓 ∣ 𝑓:𝑦⟶𝑥} |
11 | 2, 3, 4, 4, 10 | cmpo 5853 | . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
12 | 1, 11 | wceq 1348 | 1 wff ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
Colors of variables: wff set class |
This definition is referenced by: fnmap 6631 reldmmap 6633 mapvalg 6634 elmapex 6645 |
Copyright terms: Public domain | W3C validator |