Description: The value of the preimage mapping operator can be restricted to preimages of subsets of RR . (Contributed by Thierry Arnoux, 21-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | orrvccel.1 | |
|
orrvccel.2 | |
||
orrvccel.4 | |
||
Assertion | orrvcval4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orrvccel.1 | |
|
2 | orrvccel.2 | |
|
3 | orrvccel.4 | |
|
4 | domprobsiga | |
|
5 | 1 4 | syl | |
6 | retop | |
|
7 | 6 | a1i | |
8 | 1 | rrvmbfm | |
9 | 2 8 | mpbid | |
10 | df-brsiga | |
|
11 | 10 | oveq2i | |
12 | 9 11 | eleqtrdi | |
13 | 5 7 12 3 | orvcval4 | |
14 | uniretop | |
|
15 | rabeq | |
|
16 | 14 15 | ax-mp | |
17 | 16 | imaeq2i | |
18 | 13 17 | eqtr4di | |