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