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 ( 𝐿 , ℝ* , < ) )