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