Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ofr | Structured version Visualization version Unicode version |
Description: Define the function relation map. The definition is designed so that if is a binary relation, then is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.) |
Ref | Expression |
---|---|
df-ofr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cR | . . 3 | |
2 | 1 | cofr 6896 | . 2 |
3 | vx | . . . . . . 7 | |
4 | 3 | cv 1482 | . . . . . 6 |
5 | vf | . . . . . . 7 | |
6 | 5 | cv 1482 | . . . . . 6 |
7 | 4, 6 | cfv 5888 | . . . . 5 |
8 | vg | . . . . . . 7 | |
9 | 8 | cv 1482 | . . . . . 6 |
10 | 4, 9 | cfv 5888 | . . . . 5 |
11 | 7, 10, 1 | wbr 4653 | . . . 4 |
12 | 6 | cdm 5114 | . . . . 5 |
13 | 9 | cdm 5114 | . . . . 5 |
14 | 12, 13 | cin 3573 | . . . 4 |
15 | 11, 3, 14 | wral 2912 | . . 3 |
16 | 15, 5, 8 | copab 4712 | . 2 |
17 | 2, 16 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: ofreq 6900 ofrfval 6905 |
Copyright terms: Public domain | W3C validator |