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 5711 | . 2 |
3 | vx | . . . . . . 7 | |
4 | 3 | cv 1242 | . . . . . 6 |
5 | vf | . . . . . . 7 | |
6 | 5 | cv 1242 | . . . . . 6 |
7 | 4, 6 | cfv 4902 | . . . . 5 |
8 | vg | . . . . . . 7 | |
9 | 8 | cv 1242 | . . . . . 6 |
10 | 4, 9 | cfv 4902 | . . . . 5 |
11 | 7, 10, 1 | wbr 3764 | . . . 4 |
12 | 6 | cdm 4345 | . . . . 5 |
13 | 9 | cdm 4345 | . . . . 5 |
14 | 12, 13 | cin 2916 | . . . 4 |
15 | 11, 3, 14 | wral 2306 | . . 3 |
16 | 15, 5, 8 | copab 3817 | . 2 |
17 | 2, 16 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: ofreq 5715 ofrfval 5720 |
Copyright terms: Public domain | W3C validator |