Metamath Proof Explorer


Theorem i1f0rn

Description: Any simple function takes the value zero on a set of unbounded measure, so in particular this set is not empty. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion i1f0rn Fdom10ranF

Proof

Step Hyp Ref Expression
1 pnfnre +∞
2 1 neli ¬+∞
3 rembl domvol
4 mblvol domvolvol=vol*
5 3 4 ax-mp vol=vol*
6 ovolre vol*=+∞
7 5 6 eqtri vol=+∞
8 cnvimarndm F-1ranF=domF
9 i1ff Fdom1F:
10 9 fdmd Fdom1domF=
11 10 adantr Fdom1¬0ranFdomF=
12 8 11 eqtrid Fdom1¬0ranFF-1ranF=
13 12 fveq2d Fdom1¬0ranFvolF-1ranF=vol
14 i1fima2 Fdom1¬0ranFvolF-1ranF
15 13 14 eqeltrrd Fdom1¬0ranFvol
16 7 15 eqeltrrid Fdom1¬0ranF+∞
17 16 ex Fdom1¬0ranF+∞
18 2 17 mt3i Fdom10ranF