MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2cnlem1 Structured version   Visualization version   GIF version

Theorem itg2cnlem1 24368
Description: Lemma for itgcn 24451. (Contributed by Mario Carneiro, 30-Aug-2014.)
Hypotheses
Ref Expression
itg2cn.1 (𝜑𝐹:ℝ⟶(0[,)+∞))
itg2cn.2 (𝜑𝐹 ∈ MblFn)
itg2cn.3 (𝜑 → (∫2𝐹) ∈ ℝ)
Assertion
Ref Expression
itg2cnlem1 (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = (∫2𝐹))
Distinct variable groups:   𝑥,𝑛,𝐹   𝜑,𝑛,𝑥

Proof of Theorem itg2cnlem1
Dummy variables 𝑚 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6674 . . . . . . . . . 10 (𝐹𝑥) ∈ V
2 c0ex 10633 . . . . . . . . . 10 0 ∈ V
31, 2ifex 4498 . . . . . . . . 9 if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V
4 eqid 2824 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
54fvmpt2 6770 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
63, 5mpan2 690 . . . . . . . 8 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
76mpteq2dv 5148 . . . . . . 7 (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
87rneqd 5795 . . . . . 6 (𝑥 ∈ ℝ → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
98supeq1d 8907 . . . . 5 (𝑥 ∈ ℝ → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
109mpteq2ia 5143 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
11 nfcv 2982 . . . . 5 𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )
12 nfcv 2982 . . . . . . . 8 𝑥
13 nfmpt1 5150 . . . . . . . . . . 11 𝑥(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
1412, 13nfmpt 5149 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
15 nfcv 2982 . . . . . . . . . 10 𝑥𝑚
1614, 15nffv 6671 . . . . . . . . 9 𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)
17 nfcv 2982 . . . . . . . . 9 𝑥𝑦
1816, 17nffv 6671 . . . . . . . 8 𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)
1912, 18nfmpt 5149 . . . . . . 7 𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
2019nfrn 5811 . . . . . 6 𝑥ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
21 nfcv 2982 . . . . . 6 𝑥
22 nfcv 2982 . . . . . 6 𝑥 <
2320, 21, 22nfsup 8912 . . . . 5 𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )
24 fveq2 6661 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦))
2524mpteq2dv 5148 . . . . . . . 8 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)))
26 breq2 5056 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ 𝑚))
2726ifbid 4472 . . . . . . . . . . . 12 (𝑛 = 𝑚 → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
2827mpteq2dv 5148 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
2928fveq1d 6663 . . . . . . . . . 10 (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3029cbvmptv 5155 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
31 eqid 2824 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
32 reex 10626 . . . . . . . . . . . . 13 ℝ ∈ V
3332mptex 6977 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∈ V
3428, 31, 33fvmpt 6759 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
3534fveq1d 6663 . . . . . . . . . 10 (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3635mpteq2ia 5143 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3730, 36eqtr4i 2850 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
3825, 37syl6eq 2875 . . . . . . 7 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
3938rneqd 5795 . . . . . 6 (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
4039supeq1d 8907 . . . . 5 (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4111, 23, 40cbvmpt 5153 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4210, 41eqtr3i 2849 . . 3 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
43 fveq2 6661 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4443breq1d 5062 . . . . . . 7 (𝑥 = 𝑦 → ((𝐹𝑥) ≤ 𝑚 ↔ (𝐹𝑦) ≤ 𝑚))
4544, 43ifbieq1d 4473 . . . . . 6 (𝑥 = 𝑦 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4645cbvmptv 5155 . . . . 5 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4734adantl 485 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
48 nnre 11641 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
4948ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ)
5049rexrd 10689 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*)
51 elioopnf 12830 . . . . . . . . . . 11 (𝑚 ∈ ℝ* → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
5250, 51syl 17 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
53 simpr 488 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
54 itg2cn.1 . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶(0[,)+∞))
5554ffnd 6504 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
5655ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ)
57 elpreima 6819 . . . . . . . . . . . 12 (𝐹 Fn ℝ → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
5856, 57syl 17 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
5953, 58mpbirand 706 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝐹𝑦) ∈ (𝑚(,)+∞)))
60 rge0ssre 12843 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ ℝ
61 fss 6517 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
6254, 60, 61sylancl 589 . . . . . . . . . . . . 13 (𝜑𝐹:ℝ⟶ℝ)
6362adantr 484 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
6463ffvelrnda 6842 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
6564biantrurd 536 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹𝑦) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
6652, 59, 653bitr4d 314 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹𝑦)))
6766notbid 321 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹𝑦)))
68 eldif 3929 . . . . . . . . . 10 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
6968baib 539 . . . . . . . . 9 (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7069adantl 485 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7164, 49lenltd 10784 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹𝑦)))
7267, 70, 713bitr4d 314 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝐹𝑦) ≤ 𝑚))
7372ifbid 4472 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
7473mpteq2dva 5147 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0)))
7546, 47, 743eqtr4a 2885 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)))
76 difss 4094 . . . . . 6 (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ
7776a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ)
78 rembl 24147 . . . . . 6 ℝ ∈ dom vol
7978a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ dom vol)
80 fvex 6674 . . . . . . 7 (𝐹𝑦) ∈ V
8180, 2ifex 4498 . . . . . 6 if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V
8281a1i 11 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V)
83 eldifn 4090 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8483adantl 485 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8584iffalsed 4461 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = 0)
86 iftrue 4456 . . . . . . . . 9 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = (𝐹𝑦))
8786mpteq2ia 5143 . . . . . . . 8 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
88 resmpt 5892 . . . . . . . . 9 ((ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦)))
8976, 88ax-mp 5 . . . . . . . 8 ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
9087, 89eqtr4i 2850 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
9154feqmptd 6724 . . . . . . . . 9 (𝜑𝐹 = (𝑦 ∈ ℝ ↦ (𝐹𝑦)))
92 itg2cn.2 . . . . . . . . 9 (𝜑𝐹 ∈ MblFn)
9391, 92eqeltrrd 2917 . . . . . . . 8 (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn)
94 mbfima 24237 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
9592, 62, 94syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
96 cmmbl 24141 . . . . . . . . 9 ((𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
9795, 96syl 17 . . . . . . . 8 (𝜑 → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
98 mbfres 24251 . . . . . . . 8 (((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn ∧ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
9993, 97, 98syl2anc 587 . . . . . . 7 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
10090, 99eqeltrid 2920 . . . . . 6 (𝜑 → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
101100adantr 484 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10277, 79, 82, 85, 101mbfss 24253 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10375, 102eqeltrd 2916 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∈ MblFn)
10454ffvelrnda 6842 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
105 0e0icopnf 12845 . . . . . 6 0 ∈ (0[,)+∞)
106 ifcl 4494 . . . . . 6 (((𝐹𝑥) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
107104, 105, 106sylancl 589 . . . . 5 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
108107adantlr 714 . . . 4 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
10947, 108fmpt3d 6871 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞))
110 elrege0 12841 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
111104, 110sylib 221 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
112111simpld 498 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
113112adantlr 714 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
114113adantr 484 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ∈ ℝ)
115114leidd 11204 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝐹𝑥))
116 iftrue 4456 . . . . . . . . 9 ((𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
117116adantl 485 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
11848ad3antlr 730 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ)
119 peano2re 10811 . . . . . . . . . . 11 (𝑚 ∈ ℝ → (𝑚 + 1) ∈ ℝ)
120118, 119syl 17 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ)
121 simpr 488 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ 𝑚)
122118lep1d 11569 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1))
123114, 118, 120, 121, 122letrd 10795 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝑚 + 1))
124123iftrued 4458 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) = (𝐹𝑥))
125115, 117, 1243brtr4d 5084 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
126 iffalse 4459 . . . . . . . . 9 (¬ (𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
127126adantl 485 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
128111simprd 499 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
129 0le0 11735 . . . . . . . . . . 11 0 ≤ 0
130 breq2 5056 . . . . . . . . . . . 12 ((𝐹𝑥) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
131 breq2 5056 . . . . . . . . . . . 12 (0 = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ 0 ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
132130, 131ifboth 4488 . . . . . . . . . . 11 ((0 ≤ (𝐹𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
133128, 129, 132sylancl 589 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
134133adantlr 714 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
135134adantr 484 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
136127, 135eqbrtrd 5074 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
137125, 136pm2.61dan 812 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
138137ralrimiva 3177 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
1391, 2ifex 4498 . . . . . . 7 if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V
140139a1i 11 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V)
141 eqidd 2825 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
142 eqidd 2825 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
14379, 108, 140, 141, 142ofrfval2 7421 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
144138, 143mpbird 260 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
145 peano2nn 11646 . . . . . 6 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
146145adantl 485 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
147 breq2 5056 . . . . . . . 8 (𝑛 = (𝑚 + 1) → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ (𝑚 + 1)))
148147ifbid 4472 . . . . . . 7 (𝑛 = (𝑚 + 1) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
149148mpteq2dv 5148 . . . . . 6 (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
15032mptex 6977 . . . . . 6 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ∈ V
151149, 31, 150fvmpt 6759 . . . . 5 ((𝑚 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
152146, 151syl 17 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
153144, 47, 1523brtr4d 5084 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∘r ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)))
15462ffvelrnda 6842 . . . 4 ((𝜑𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
15534adantl 485 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
156155fveq1d 6663 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
157112leidd 11204 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ (𝐹𝑥))
158 breq1 5055 . . . . . . . . . . . . . 14 ((𝐹𝑥) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
159 breq1 5055 . . . . . . . . . . . . . 14 (0 = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
160158, 159ifboth 4488 . . . . . . . . . . . . 13 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
161157, 128, 160syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
162161adantlr 714 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
163162ralrimiva 3177 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
16432a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ V)
1651, 2ifex 4498 . . . . . . . . . . . 12 if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V
166165a1i 11 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V)
16754feqmptd 6724 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
168167adantr 484 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
169164, 166, 113, 141, 168ofrfval2 7421 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘r𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
170163, 169mpbird 260 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘r𝐹)
171166fmpttd 6870 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶V)
172171ffnd 6504 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) Fn ℝ)
17355adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹 Fn ℝ)
174 inidm 4180 . . . . . . . . . 10 (ℝ ∩ ℝ) = ℝ
175 eqidd 2825 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
176 eqidd 2825 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) = (𝐹𝑦))
177172, 173, 164, 164, 174, 175, 176ofrfval 7411 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘r𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦)))
178170, 177mpbid 235 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
179178r19.21bi 3203 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
180179an32s 651 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
181156, 180eqbrtrd 5074 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
182181ralrimiva 3177 . . . 4 ((𝜑𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
183 brralrspcev 5112 . . . 4 (((𝐹𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
184154, 182, 183syl2anc 587 . . 3 ((𝜑𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
18528fveq2d 6665 . . . . . . 7 (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
186185cbvmptv 5155 . . . . . 6 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
18734fveq2d 6665 . . . . . . 7 (𝑚 ∈ ℕ → (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
188187mpteq2ia 5143 . . . . . 6 (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
189186, 188eqtr4i 2850 . . . . 5 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
190189rneqi 5794 . . . 4 ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
191190supeq1i 8908 . . 3 sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))), ℝ*, < )
19242, 103, 109, 153, 184, 191itg2mono 24360 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ))
193 eqid 2824 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
19427, 193, 165fvmpt 6759 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
195194adantl 485 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
196161adantr 484 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
197195, 196eqbrtrd 5074 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
198197ralrimiva 3177 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
1993a1i 11 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V)
200199fmpttd 6870 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶V)
201200ffnd 6504 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
202 breq1 5055 . . . . . . . . . 10 (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
203202ralrn 6845 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
204201, 203syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
205198, 204mpbird 260 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥))
206112adantr 484 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑥) ∈ ℝ)
207 0re 10641 . . . . . . . . . . 11 0 ∈ ℝ
208 ifcl 4494 . . . . . . . . . . 11 (((𝐹𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
209206, 207, 208sylancl 589 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
210209fmpttd 6870 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶ℝ)
211210frnd 6510 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ)
212 1nn 11645 . . . . . . . . . 10 1 ∈ ℕ
213193, 209dmmptd 6482 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ℕ)
214212, 213eleqtrrid 2923 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
215 n0i 4282 . . . . . . . . . 10 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
216 dm0rn0 5782 . . . . . . . . . . 11 (dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
217216necon3bbii 3061 . . . . . . . . . 10 (¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
218215, 217sylib 221 . . . . . . . . 9 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
219214, 218syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
220 brralrspcev 5112 . . . . . . . . 9 (((𝐹𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
221112, 205, 220syl2anc 587 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
222 suprleub 11603 . . . . . . . 8 (((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) ∧ (𝐹𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
223211, 219, 221, 112, 222syl31anc 1370 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
224205, 223mpbird 260 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥))
225 arch 11891 . . . . . . . . 9 ((𝐹𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
226112, 225syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
227194ad2antrl 727 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
228 ltle 10727 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
229112, 48, 228syl2an 598 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
230229impr 458 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ≤ 𝑚)
231230iftrued 4458 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
232227, 231eqtrd 2859 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = (𝐹𝑥))
233201adantr 484 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
234 simprl 770 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → 𝑚 ∈ ℕ)
235 fnfvelrn 6839 . . . . . . . . . 10 (((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
236233, 234, 235syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
237232, 236eqeltrrd 2917 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
238226, 237rexlimddv 3283 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
239211, 219, 221, 238suprubd 11599 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
240211, 219, 221suprcld 11600 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ∈ ℝ)
241240, 112letri3d 10780 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ∧ (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))))
242224, 239, 241mpbir2and 712 . . . . 5 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥))
243242mpteq2dva 5147 . . . 4 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
244243, 167eqtr4d 2862 . . 3 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = 𝐹)
245244fveq2d 6665 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = (∫2𝐹))
246192, 245eqtr3d 2861 1 (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = (∫2𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3014  wral 3133  wrex 3134  Vcvv 3480  cdif 3916  wss 3919  c0 4276  ifcif 4450   class class class wbr 5052  cmpt 5132  ccnv 5541  dom cdm 5542  ran crn 5543  cres 5544  cima 5545   Fn wfn 6338  wf 6339  cfv 6343  (class class class)co 7149  r cofr 7402  supcsup 8901  cr 10534  0cc0 10535  1c1 10536   + caddc 10538  +∞cpnf 10670  *cxr 10672   < clt 10673  cle 10674  cn 11634  (,)cioo 12735  [,)cico 12737  volcvol 24070  MblFncmbf 24221  2citg2 24223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cc 9855  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8285  df-map 8404  df-pm 8405  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-acn 9368  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-n0 11895  df-z 11979  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-rlim 14846  df-sum 15043  df-rest 16696  df-topgen 16717  df-psmet 20537  df-xmet 20538  df-met 20539  df-bl 20540  df-mopn 20541  df-top 21502  df-topon 21519  df-bases 21554  df-cmp 21995  df-ovol 24071  df-vol 24072  df-mbf 24226  df-itg1 24227  df-itg2 24228
This theorem is referenced by:  itg2cn  24370
  Copyright terms: Public domain W3C validator