Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-ofc | Structured version Visualization version GIF version |
Description: Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘𝑓/𝑐𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
Ref | Expression |
---|---|
df-ofc | ⊢ ∘𝑓/𝑐𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cR | . . 3 class 𝑅 | |
2 | 1 | cofc 29484 | . 2 class ∘𝑓/𝑐𝑅 |
3 | vf | . . 3 setvar 𝑓 | |
4 | vc | . . 3 setvar 𝑐 | |
5 | cvv 3173 | . . 3 class V | |
6 | vx | . . . 4 setvar 𝑥 | |
7 | 3 | cv 1474 | . . . . 5 class 𝑓 |
8 | 7 | cdm 5038 | . . . 4 class dom 𝑓 |
9 | 6 | cv 1474 | . . . . . 6 class 𝑥 |
10 | 9, 7 | cfv 5804 | . . . . 5 class (𝑓‘𝑥) |
11 | 4 | cv 1474 | . . . . 5 class 𝑐 |
12 | 10, 11, 1 | co 6549 | . . . 4 class ((𝑓‘𝑥)𝑅𝑐) |
13 | 6, 8, 12 | cmpt 4643 | . . 3 class (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)) |
14 | 3, 4, 5, 5, 13 | cmpt2 6551 | . 2 class (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐))) |
15 | 2, 14 | wceq 1475 | 1 wff ∘𝑓/𝑐𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐))) |
Colors of variables: wff setvar class |
This definition is referenced by: ofceq 29486 ofcfval 29487 ofcfval3 29491 |
Copyright terms: Public domain | W3C validator |