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	⊢ ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		pnfnre	⊢ +∞ ∉ ℝ
2	1	neli	⊢ ¬ +∞ ∈ ℝ
3		rembl	⊢ ℝ ∈ dom vol
4		mblvol	⊢ ( ℝ ∈ dom vol → ( vol ‘ ℝ ) = ( vol* ‘ ℝ ) )
5	3 4	ax-mp	⊢ ( vol ‘ ℝ ) = ( vol* ‘ ℝ )
6		ovolre	⊢ ( vol* ‘ ℝ ) = +∞
7	5 6	eqtri	⊢ ( vol ‘ ℝ ) = +∞
8		cnvimarndm	⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
9		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
10	9	fdmd	⊢ ( 𝐹 ∈ dom ∫1 → dom 𝐹 = ℝ )
11	10	adantr	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → dom 𝐹 = ℝ )
12	8 11	syl5eq	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ ran 𝐹 ) = ℝ )
13	12	fveq2d	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( vol ‘ ℝ ) )
14		i1fima2	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ( ◡ 𝐹 “ ran 𝐹 ) ) ∈ ℝ )
15	13 14	eqeltrrd	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ℝ ) ∈ ℝ )
16	7 15	eqeltrrid	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → +∞ ∈ ℝ )
17	16	ex	⊢ ( 𝐹 ∈ dom ∫1 → ( ¬ 0 ∈ ran 𝐹 → +∞ ∈ ℝ ) )
18	2 17	mt3i	⊢ ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )