Metamath Proof Explorer


Theorem itg2val

Description: Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypothesis itg2val.1 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝐹𝑥 = ( ∫1𝑔 ) ) }
Assertion itg2val ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2𝐹 ) = sup ( 𝐿 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 itg2val.1 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝐹𝑥 = ( ∫1𝑔 ) ) }
2 xrltso < Or ℝ*
3 2 supex sup ( 𝐿 , ℝ* , < ) ∈ V
4 reex ℝ ∈ V
5 ovex ( 0 [,] +∞ ) ∈ V
6 breq2 ( 𝑓 = 𝐹 → ( 𝑔r𝑓𝑔r𝐹 ) )
7 6 anbi1d ( 𝑓 = 𝐹 → ( ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) ↔ ( 𝑔r𝐹𝑥 = ( ∫1𝑔 ) ) ) )
8 7 rexbidv ( 𝑓 = 𝐹 → ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝐹𝑥 = ( ∫1𝑔 ) ) ) )
9 8 abbidv ( 𝑓 = 𝐹 → { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) } = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝐹𝑥 = ( ∫1𝑔 ) ) } )
10 9 1 eqtr4di ( 𝑓 = 𝐹 → { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) } = 𝐿 )
11 10 supeq1d ( 𝑓 = 𝐹 → sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) } , ℝ* , < ) = sup ( 𝐿 , ℝ* , < ) )
12 df-itg2 2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔r𝑓𝑥 = ( ∫1𝑔 ) ) } , ℝ* , < ) )
13 3 4 5 11 12 fvmptmap ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2𝐹 ) = sup ( 𝐿 , ℝ* , < ) )