Description: Preimage maps produced by the "greater than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | orvcgteel.1 | |
|
orvcgteel.2 | |
||
orvcgteel.3 | |
||
Assertion | orvcgteel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orvcgteel.1 | |
|
2 | orvcgteel.2 | |
|
3 | orvcgteel.3 | |
|
4 | simpr | |
|
5 | 3 | adantr | |
6 | brcnvg | |
|
7 | 4 5 6 | syl2anc | |
8 | 7 | pm5.32da | |
9 | rexr | |
|
10 | 9 | ad2antrl | |
11 | simprr | |
|
12 | ltpnf | |
|
13 | 12 | ad2antrl | |
14 | 11 13 | jca | |
15 | 10 14 | jca | |
16 | simprl | |
|
17 | 3 | adantr | |
18 | simprrl | |
|
19 | simprrr | |
|
20 | xrre3 | |
|
21 | 16 17 18 19 20 | syl22anc | |
22 | 21 18 | jca | |
23 | 15 22 | impbida | |
24 | 8 23 | bitrd | |
25 | 24 | rabbidva2 | |
26 | 3 | rexrd | |
27 | pnfxr | |
|
28 | icoval | |
|
29 | 26 27 28 | sylancl | |
30 | 25 29 | eqtr4d | |
31 | icopnfcld | |
|
32 | 3 31 | syl | |
33 | 30 32 | eqeltrd | |
34 | 1 2 3 33 | orrvccel | |