Metamath Proof Explorer


Theorem icombl1

Description: A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion icombl1 AA+∞domvol

Proof

Step Hyp Ref Expression
1 rexr AA*
2 pnfxr +∞*
3 2 a1i A+∞*
4 ltpnf AA<+∞
5 snunioo A*+∞*A<+∞AA+∞=A+∞
6 1 3 4 5 syl3anc AAA+∞=A+∞
7 snssi AA
8 ovolsn Avol*A=0
9 nulmbl Avol*A=0Adomvol
10 7 8 9 syl2anc AAdomvol
11 ioombl1 A*A+∞domvol
12 1 11 syl AA+∞domvol
13 unmbl AdomvolA+∞domvolAA+∞domvol
14 10 12 13 syl2anc AAA+∞domvol
15 6 14 eqeltrrd AA+∞domvol