Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-map | Structured version Visualization version GIF version |
Description: Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑m 𝐵) (see mapval 8634). 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 (𝐴 ↑m 𝐵). 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 | ⊢ ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmap 8622 | . 2 class ↑m | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cvv 3431 | . . 3 class V | |
5 | 3 | cv 1537 | . . . . 5 class 𝑦 |
6 | 2 | cv 1537 | . . . . 5 class 𝑥 |
7 | vf | . . . . . 6 setvar 𝑓 | |
8 | 7 | cv 1537 | . . . . 5 class 𝑓 |
9 | 5, 6, 8 | wf 6431 | . . . 4 wff 𝑓:𝑦⟶𝑥 |
10 | 9, 7 | cab 2712 | . . 3 class {𝑓 ∣ 𝑓:𝑦⟶𝑥} |
11 | 2, 3, 4, 4, 10 | cmpo 7284 | . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
12 | 1, 11 | wceq 1538 | 1 wff ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
Colors of variables: wff setvar class |
This definition is referenced by: fnmap 8629 reldmmap 8631 mapvalg 8632 naryfval 45995 |
Copyright terms: Public domain | W3C validator |