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

Theorem itg2cnlem1 23969
Description: Lemma for itgcn 24050. (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 6461 . . . . . . . . . 10 (𝐹𝑥) ∈ V
2 c0ex 10372 . . . . . . . . . 10 0 ∈ V
31, 2ifex 4355 . . . . . . . . 9 if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V
4 eqid 2778 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
54fvmpt2 6554 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
63, 5mpan2 681 . . . . . . . 8 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
76mpteq2dv 4982 . . . . . . 7 (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
87rneqd 5600 . . . . . 6 (𝑥 ∈ ℝ → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
98supeq1d 8642 . . . . 5 (𝑥 ∈ ℝ → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
109mpteq2ia 4977 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
11 nfcv 2934 . . . . 5 𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )
12 nfcv 2934 . . . . . . . 8 𝑥
13 nfmpt1 4984 . . . . . . . . . . 11 𝑥(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
1412, 13nfmpt 4983 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
15 nfcv 2934 . . . . . . . . . 10 𝑥𝑚
1614, 15nffv 6458 . . . . . . . . 9 𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)
17 nfcv 2934 . . . . . . . . 9 𝑥𝑦
1816, 17nffv 6458 . . . . . . . 8 𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)
1912, 18nfmpt 4983 . . . . . . 7 𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
2019nfrn 5616 . . . . . 6 𝑥ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
21 nfcv 2934 . . . . . 6 𝑥
22 nfcv 2934 . . . . . 6 𝑥 <
2320, 21, 22nfsup 8647 . . . . 5 𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )
24 fveq2 6448 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦))
2524mpteq2dv 4982 . . . . . . . 8 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)))
26 breq2 4892 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ 𝑚))
2726ifbid 4329 . . . . . . . . . . . 12 (𝑛 = 𝑚 → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
2827mpteq2dv 4982 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
2928fveq1d 6450 . . . . . . . . . 10 (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3029cbvmptv 4987 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
31 eqid 2778 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
32 reex 10365 . . . . . . . . . . . . 13 ℝ ∈ V
3332mptex 6760 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∈ V
3428, 31, 33fvmpt 6544 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
3534fveq1d 6450 . . . . . . . . . 10 (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3635mpteq2ia 4977 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3730, 36eqtr4i 2805 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
3825, 37syl6eq 2830 . . . . . . 7 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
3938rneqd 5600 . . . . . 6 (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
4039supeq1d 8642 . . . . 5 (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4111, 23, 40cbvmpt 4986 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4210, 41eqtr3i 2804 . . 3 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
43 fveq2 6448 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4443breq1d 4898 . . . . . . 7 (𝑥 = 𝑦 → ((𝐹𝑥) ≤ 𝑚 ↔ (𝐹𝑦) ≤ 𝑚))
4544, 43ifbieq1d 4330 . . . . . 6 (𝑥 = 𝑦 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4645cbvmptv 4987 . . . . 5 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4734adantl 475 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
48 nnre 11386 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
4948ad2antlr 717 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ)
5049rexrd 10428 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*)
51 elioopnf 12584 . . . . . . . . . . 11 (𝑚 ∈ ℝ* → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
5250, 51syl 17 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
53 itg2cn.1 . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶(0[,)+∞))
5453ffnd 6294 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
5554ad2antrr 716 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ)
56 elpreima 6602 . . . . . . . . . . . 12 (𝐹 Fn ℝ → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
5755, 56syl 17 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
58 simpr 479 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
5958biantrurd 528 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
6057, 59bitr4d 274 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝐹𝑦) ∈ (𝑚(,)+∞)))
61 rge0ssre 12598 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ ℝ
62 fss 6306 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
6353, 61, 62sylancl 580 . . . . . . . . . . . . 13 (𝜑𝐹:ℝ⟶ℝ)
6463adantr 474 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
6564ffvelrnda 6625 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
6665biantrurd 528 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹𝑦) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
6752, 60, 663bitr4d 303 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹𝑦)))
6867notbid 310 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹𝑦)))
69 eldif 3802 . . . . . . . . . 10 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7069baib 531 . . . . . . . . 9 (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7170adantl 475 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7265, 49lenltd 10524 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹𝑦)))
7368, 71, 723bitr4d 303 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝐹𝑦) ≤ 𝑚))
7473ifbid 4329 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
7574mpteq2dva 4981 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0)))
7646, 47, 753eqtr4a 2840 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)))
77 difss 3960 . . . . . 6 (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ
7877a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ)
79 rembl 23748 . . . . . 6 ℝ ∈ dom vol
8079a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ dom vol)
81 fvex 6461 . . . . . . 7 (𝐹𝑦) ∈ V
8281, 2ifex 4355 . . . . . 6 if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V
8382a1i 11 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V)
84 eldifn 3956 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8584adantl 475 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8685iffalsed 4318 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = 0)
87 iftrue 4313 . . . . . . . . 9 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = (𝐹𝑦))
8887mpteq2ia 4977 . . . . . . . 8 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
89 resmpt 5701 . . . . . . . . 9 ((ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦)))
9077, 89ax-mp 5 . . . . . . . 8 ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
9188, 90eqtr4i 2805 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
9253feqmptd 6511 . . . . . . . . 9 (𝜑𝐹 = (𝑦 ∈ ℝ ↦ (𝐹𝑦)))
93 itg2cn.2 . . . . . . . . 9 (𝜑𝐹 ∈ MblFn)
9492, 93eqeltrrd 2860 . . . . . . . 8 (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn)
95 mbfima 23838 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
9693, 63, 95syl2anc 579 . . . . . . . . 9 (𝜑 → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
97 cmmbl 23742 . . . . . . . . 9 ((𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
9896, 97syl 17 . . . . . . . 8 (𝜑 → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
99 mbfres 23852 . . . . . . . 8 (((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn ∧ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
10094, 98, 99syl2anc 579 . . . . . . 7 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
10191, 100syl5eqel 2863 . . . . . 6 (𝜑 → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
102101adantr 474 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10378, 80, 83, 86, 102mbfss 23854 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10476, 103eqeltrd 2859 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∈ MblFn)
10553ffvelrnda 6625 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
106 0e0icopnf 12600 . . . . . . 7 0 ∈ (0[,)+∞)
107 ifcl 4351 . . . . . . 7 (((𝐹𝑥) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
108105, 106, 107sylancl 580 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
109108adantlr 705 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
110109fmpttd 6651 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶(0[,)+∞))
11147feq1d 6278 . . . 4 ((𝜑𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶(0[,)+∞)))
112110, 111mpbird 249 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞))
113 elrege0 12596 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
114105, 113sylib 210 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
115114simpld 490 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
116115adantlr 705 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
117116adantr 474 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ∈ ℝ)
118117leidd 10943 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝐹𝑥))
119 iftrue 4313 . . . . . . . . 9 ((𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
120119adantl 475 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
12148ad3antlr 721 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ)
122 peano2re 10551 . . . . . . . . . . 11 (𝑚 ∈ ℝ → (𝑚 + 1) ∈ ℝ)
123121, 122syl 17 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ)
124 simpr 479 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ 𝑚)
125121lep1d 11311 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1))
126117, 121, 123, 124, 125letrd 10535 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝑚 + 1))
127126iftrued 4315 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) = (𝐹𝑥))
128118, 120, 1273brtr4d 4920 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
129 iffalse 4316 . . . . . . . . 9 (¬ (𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
130129adantl 475 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
131114simprd 491 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
132 0le0 11487 . . . . . . . . . . 11 0 ≤ 0
133 breq2 4892 . . . . . . . . . . . 12 ((𝐹𝑥) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
134 breq2 4892 . . . . . . . . . . . 12 (0 = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ 0 ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
135133, 134ifboth 4345 . . . . . . . . . . 11 ((0 ≤ (𝐹𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
136131, 132, 135sylancl 580 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
137136adantlr 705 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
138137adantr 474 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
139130, 138eqbrtrd 4910 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
140128, 139pm2.61dan 803 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
141140ralrimiva 3148 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
1421, 2ifex 4355 . . . . . . 7 if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V
143142a1i 11 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V)
144 eqidd 2779 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
145 eqidd 2779 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
14680, 109, 143, 144, 145ofrfval2 7194 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
147141, 146mpbird 249 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
148 peano2nn 11392 . . . . . 6 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
149148adantl 475 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
150 breq2 4892 . . . . . . . 8 (𝑛 = (𝑚 + 1) → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ (𝑚 + 1)))
151150ifbid 4329 . . . . . . 7 (𝑛 = (𝑚 + 1) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
152151mpteq2dv 4982 . . . . . 6 (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
15332mptex 6760 . . . . . 6 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ∈ V
154152, 31, 153fvmpt 6544 . . . . 5 ((𝑚 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
155149, 154syl 17 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
156147, 47, 1553brtr4d 4920 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∘𝑟 ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)))
15763ffvelrnda 6625 . . . 4 ((𝜑𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
15834adantl 475 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
159158fveq1d 6450 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
160115leidd 10943 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ (𝐹𝑥))
161 breq1 4891 . . . . . . . . . . . . . 14 ((𝐹𝑥) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
162 breq1 4891 . . . . . . . . . . . . . 14 (0 = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
163161, 162ifboth 4345 . . . . . . . . . . . . 13 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
164160, 131, 163syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
165164adantlr 705 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
166165ralrimiva 3148 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
16732a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ V)
1681, 2ifex 4355 . . . . . . . . . . . 12 if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V
169168a1i 11 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V)
17053feqmptd 6511 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
171170adantr 474 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
172167, 169, 116, 144, 171ofrfval2 7194 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
173166, 172mpbird 249 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹)
174169fmpttd 6651 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶V)
175174ffnd 6294 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) Fn ℝ)
17654adantr 474 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹 Fn ℝ)
177 inidm 4043 . . . . . . . . . 10 (ℝ ∩ ℝ) = ℝ
178 eqidd 2779 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
179 eqidd 2779 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) = (𝐹𝑦))
180175, 176, 167, 167, 177, 178, 179ofrfval 7184 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦)))
181173, 180mpbid 224 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
182181r19.21bi 3114 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
183182an32s 642 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
184159, 183eqbrtrd 4910 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
185184ralrimiva 3148 . . . 4 ((𝜑𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
186 brralrspcev 4948 . . . 4 (((𝐹𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
187157, 185, 186syl2anc 579 . . 3 ((𝜑𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
18828fveq2d 6452 . . . . . . 7 (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
189188cbvmptv 4987 . . . . . 6 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
19034fveq2d 6452 . . . . . . 7 (𝑚 ∈ ℕ → (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
191190mpteq2ia 4977 . . . . . 6 (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
192189, 191eqtr4i 2805 . . . . 5 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
193192rneqi 5599 . . . 4 ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
194193supeq1i 8643 . . 3 sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))), ℝ*, < )
19542, 104, 112, 156, 187, 194itg2mono 23961 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ))
196 eqid 2778 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
19727, 196, 168fvmpt 6544 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
198197adantl 475 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
199164adantr 474 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
200198, 199eqbrtrd 4910 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
201200ralrimiva 3148 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
2023a1i 11 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V)
203202fmpttd 6651 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶V)
204203ffnd 6294 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
205 breq1 4891 . . . . . . . . . 10 (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
206205ralrn 6628 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
207204, 206syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
208201, 207mpbird 249 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥))
209115adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑥) ∈ ℝ)
210 0re 10380 . . . . . . . . . . 11 0 ∈ ℝ
211 ifcl 4351 . . . . . . . . . . 11 (((𝐹𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
212209, 210, 211sylancl 580 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
213212fmpttd 6651 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶ℝ)
214213frnd 6300 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ)
215 1nn 11391 . . . . . . . . . 10 1 ∈ ℕ
216196, 212dmmptd 6272 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ℕ)
217215, 216syl5eleqr 2866 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
218 n0i 4148 . . . . . . . . . 10 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
219 dm0rn0 5589 . . . . . . . . . . 11 (dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
220219necon3bbii 3016 . . . . . . . . . 10 (¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
221218, 220sylib 210 . . . . . . . . 9 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
222217, 221syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
223 brralrspcev 4948 . . . . . . . . 9 (((𝐹𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
224115, 208, 223syl2anc 579 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
225 suprleub 11347 . . . . . . . 8 (((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) ∧ (𝐹𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
226214, 222, 224, 115, 225syl31anc 1441 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
227208, 226mpbird 249 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥))
228 arch 11643 . . . . . . . . 9 ((𝐹𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
229115, 228syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
230197ad2antrl 718 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
231 ltle 10467 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
232115, 48, 231syl2an 589 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
233232impr 448 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ≤ 𝑚)
234233iftrued 4315 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
235230, 234eqtrd 2814 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = (𝐹𝑥))
236204adantr 474 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
237 simprl 761 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → 𝑚 ∈ ℕ)
238 fnfvelrn 6622 . . . . . . . . . 10 (((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
239236, 237, 238syl2anc 579 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
240235, 239eqeltrrd 2860 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
241229, 240rexlimddv 3218 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
242 suprub 11342 . . . . . . 7 (((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) ∧ (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) → (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
243214, 222, 224, 241, 242syl31anc 1441 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
244 suprcl 11341 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ∈ ℝ)
245214, 222, 224, 244syl3anc 1439 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ∈ ℝ)
246245, 115letri3d 10520 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ∧ (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))))
247227, 243, 246mpbir2and 703 . . . . 5 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥))
248247mpteq2dva 4981 . . . 4 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
249248, 170eqtr4d 2817 . . 3 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = 𝐹)
250249fveq2d 6452 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = (∫2𝐹))
251195, 250eqtr3d 2816 1 (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = (∫2𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  cdif 3789  wss 3792  c0 4141  ifcif 4307   class class class wbr 4888  cmpt 4967  ccnv 5356  dom cdm 5357  ran crn 5358  cres 5359  cima 5360   Fn wfn 6132  wf 6133  cfv 6137  (class class class)co 6924  𝑟 cofr 7175  supcsup 8636  cr 10273  0cc0 10274  1c1 10275   + caddc 10277  +∞cpnf 10410  *cxr 10412   < clt 10413  cle 10414  cn 11378  (,)cioo 12491  [,)cico 12493  volcvol 23671  MblFncmbf 23822  2citg2 23824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cc 9594  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-disj 4857  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-ofr 7177  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-omul 7850  df-er 8028  df-map 8144  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-acn 9103  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-n0 11647  df-z 11733  df-uz 11997  df-q 12100  df-rp 12142  df-xneg 12261  df-xadd 12262  df-xmul 12263  df-ioo 12495  df-ioc 12496  df-ico 12497  df-icc 12498  df-fz 12648  df-fzo 12789  df-fl 12916  df-seq 13124  df-exp 13183  df-hash 13440  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-clim 14631  df-rlim 14632  df-sum 14829  df-rest 16473  df-topgen 16494  df-psmet 20138  df-xmet 20139  df-met 20140  df-bl 20141  df-mopn 20142  df-top 21110  df-topon 21127  df-bases 21162  df-cmp 21603  df-ovol 23672  df-vol 23673  df-mbf 23827  df-itg1 23828  df-itg2 23829
This theorem is referenced by:  itg2cn  23971
  Copyright terms: Public domain W3C validator