Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ofr | 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 5731 | . 2 |
3 | vx | . . . . . . 7 | |
4 | 3 | cv 1283 | . . . . . 6 |
5 | vf | . . . . . . 7 | |
6 | 5 | cv 1283 | . . . . . 6 |
7 | 4, 6 | cfv 4922 | . . . . 5 |
8 | vg | . . . . . . 7 | |
9 | 8 | cv 1283 | . . . . . 6 |
10 | 4, 9 | cfv 4922 | . . . . 5 |
11 | 7, 10, 1 | wbr 3785 | . . . 4 |
12 | 6 | cdm 4363 | . . . . 5 |
13 | 9 | cdm 4363 | . . . . 5 |
14 | 12, 13 | cin 2972 | . . . 4 |
15 | 11, 3, 14 | wral 2348 | . . 3 |
16 | 15, 5, 8 | copab 3838 | . 2 |
17 | 2, 16 | wceq 1284 | 1 |
Colors of variables: wff set class |
This definition is referenced by: ofreq 5735 ofrfval 5740 |
Copyright terms: Public domain | W3C validator |