Description: A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | icombl1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr | |
|
2 | pnfxr | |
|
3 | 2 | a1i | |
4 | ltpnf | |
|
5 | snunioo | |
|
6 | 1 3 4 5 | syl3anc | |
7 | snssi | |
|
8 | ovolsn | |
|
9 | nulmbl | |
|
10 | 7 8 9 | syl2anc | |
11 | ioombl1 | |
|
12 | 1 11 | syl | |
13 | unmbl | |
|
14 | 10 12 13 | syl2anc | |
15 | 6 14 | eqeltrrd | |