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

Theorem itg2cnlem1 23509
Description: Lemma for itgcn 23590. (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 6188 . . . . . . . . . 10 (𝐹𝑥) ∈ V
2 c0ex 10019 . . . . . . . . . 10 0 ∈ V
31, 2ifex 4147 . . . . . . . . 9 if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V
4 eqid 2620 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
54fvmpt2 6278 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
63, 5mpan2 706 . . . . . . . 8 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
76mpteq2dv 4736 . . . . . . 7 (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
87rneqd 5342 . . . . . 6 (𝑥 ∈ ℝ → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
98supeq1d 8337 . . . . 5 (𝑥 ∈ ℝ → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
109mpteq2ia 4731 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
11 nfcv 2762 . . . . 5 𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )
12 nfcv 2762 . . . . . . . 8 𝑥
13 nfmpt1 4738 . . . . . . . . . . 11 𝑥(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
1412, 13nfmpt 4737 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
15 nfcv 2762 . . . . . . . . . 10 𝑥𝑚
1614, 15nffv 6185 . . . . . . . . 9 𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)
17 nfcv 2762 . . . . . . . . 9 𝑥𝑦
1816, 17nffv 6185 . . . . . . . 8 𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)
1912, 18nfmpt 4737 . . . . . . 7 𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
2019nfrn 5357 . . . . . 6 𝑥ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
21 nfcv 2762 . . . . . 6 𝑥
22 nfcv 2762 . . . . . 6 𝑥 <
2320, 21, 22nfsup 8342 . . . . 5 𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )
24 fveq2 6178 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦))
2524mpteq2dv 4736 . . . . . . . 8 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)))
26 breq2 4648 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ 𝑚))
2726ifbid 4099 . . . . . . . . . . . 12 (𝑛 = 𝑚 → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
2827mpteq2dv 4736 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
2928fveq1d 6180 . . . . . . . . . 10 (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3029cbvmptv 4741 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
31 eqid 2620 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
32 reex 10012 . . . . . . . . . . . . 13 ℝ ∈ V
3332mptex 6471 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∈ V
3428, 31, 33fvmpt 6269 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
3534fveq1d 6180 . . . . . . . . . 10 (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3635mpteq2ia 4731 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
3730, 36eqtr4i 2645 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦))
3825, 37syl6eq 2670 . . . . . . 7 (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
3938rneqd 5342 . . . . . 6 (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)))
4039supeq1d 8337 . . . . 5 (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4111, 23, 40cbvmpt 4740 . . . 4 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
4210, 41eqtr3i 2644 . . 3 (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ))
43 fveq2 6178 . . . . . . . 8 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
4443breq1d 4654 . . . . . . 7 (𝑥 = 𝑦 → ((𝐹𝑥) ≤ 𝑚 ↔ (𝐹𝑦) ≤ 𝑚))
4544, 43ifbieq1d 4100 . . . . . 6 (𝑥 = 𝑦 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4645cbvmptv 4741 . . . . 5 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
4734adantl 482 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
48 nnre 11012 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
4948ad2antlr 762 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ)
5049rexrd 10074 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*)
51 elioopnf 12252 . . . . . . . . . . 11 (𝑚 ∈ ℝ* → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
5250, 51syl 17 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
53 itg2cn.1 . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶(0[,)+∞))
54 ffn 6032 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
5553, 54syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 Fn ℝ)
5655ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ)
57 elpreima 6323 . . . . . . . . . . . 12 (𝐹 Fn ℝ → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
5856, 57syl 17 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
59 simpr 477 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
6059biantrurd 529 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ∈ (𝑚(,)+∞) ↔ (𝑦 ∈ ℝ ∧ (𝐹𝑦) ∈ (𝑚(,)+∞))))
6158, 60bitr4d 271 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ (𝐹𝑦) ∈ (𝑚(,)+∞)))
62 rge0ssre 12265 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ ℝ
63 fss 6043 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
6453, 62, 63sylancl 693 . . . . . . . . . . . . 13 (𝜑𝐹:ℝ⟶ℝ)
6564adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
6665ffvelrnda 6345 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
6766biantrurd 529 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹𝑦) ↔ ((𝐹𝑦) ∈ ℝ ∧ 𝑚 < (𝐹𝑦))))
6852, 61, 673bitr4d 300 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹𝑦)))
6968notbid 308 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹𝑦)))
70 eldif 3577 . . . . . . . . . 10 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7170baib 943 . . . . . . . . 9 (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7271adantl 482 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (𝐹 “ (𝑚(,)+∞))))
7366, 49lenltd 10168 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹𝑦)))
7469, 72, 733bitr4d 300 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↔ (𝐹𝑦) ≤ 𝑚))
7574ifbid 4099 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0))
7675mpteq2dva 4735 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹𝑦) ≤ 𝑚, (𝐹𝑦), 0)))
7746, 47, 763eqtr4a 2680 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)))
78 difss 3729 . . . . . 6 (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ
7978a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ)
80 rembl 23289 . . . . . 6 ℝ ∈ dom vol
8180a1i 11 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ dom vol)
82 fvex 6188 . . . . . . 7 (𝐹𝑦) ∈ V
8382, 2ifex 4147 . . . . . 6 if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V
8483a1i 11 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) ∈ V)
85 eldifn 3725 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8685adantl 482 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
8786iffalsed 4088 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = 0)
88 iftrue 4083 . . . . . . . . 9 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0) = (𝐹𝑦))
8988mpteq2ia 4731 . . . . . . . 8 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
90 resmpt 5437 . . . . . . . . 9 ((ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦)))
9178, 90ax-mp 5 . . . . . . . 8 ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ (𝐹𝑦))
9289, 91eqtr4i 2645 . . . . . . 7 (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))))
9353feqmptd 6236 . . . . . . . . 9 (𝜑𝐹 = (𝑦 ∈ ℝ ↦ (𝐹𝑦)))
94 itg2cn.2 . . . . . . . . 9 (𝜑𝐹 ∈ MblFn)
9593, 94eqeltrrd 2700 . . . . . . . 8 (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn)
96 mbfima 23380 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
9794, 64, 96syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐹 “ (𝑚(,)+∞)) ∈ dom vol)
98 cmmbl 23283 . . . . . . . . 9 ((𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
9997, 98syl 17 . . . . . . . 8 (𝜑 → (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol)
100 mbfres 23392 . . . . . . . 8 (((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ∈ MblFn ∧ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
10195, 99, 100syl2anc 692 . . . . . . 7 (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹𝑦)) ↾ (ℝ ∖ (𝐹 “ (𝑚(,)+∞)))) ∈ MblFn)
10292, 101syl5eqel 2703 . . . . . 6 (𝜑 → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
103102adantr 481 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10479, 81, 84, 87, 103mbfss 23394 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (𝐹 “ (𝑚(,)+∞))), (𝐹𝑦), 0)) ∈ MblFn)
10577, 104eqeltrd 2699 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∈ MblFn)
10653ffvelrnda 6345 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
107 0e0icopnf 12267 . . . . . . 7 0 ∈ (0[,)+∞)
108 ifcl 4121 . . . . . . 7 (((𝐹𝑥) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
109106, 107, 108sylancl 693 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
110109adantlr 750 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ (0[,)+∞))
111 eqid 2620 . . . . 5 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
112110, 111fmptd 6371 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶(0[,)+∞))
11347feq1d 6017 . . . 4 ((𝜑𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶(0[,)+∞)))
114112, 113mpbird 247 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞))
115 elrege0 12263 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
116106, 115sylib 208 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
117116simpld 475 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
118117adantlr 750 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
119118adantr 481 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ∈ ℝ)
120119leidd 10579 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝐹𝑥))
121 iftrue 4083 . . . . . . . . 9 ((𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
122121adantl 482 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
12348ad3antlr 766 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ)
124 peano2re 10194 . . . . . . . . . . 11 (𝑚 ∈ ℝ → (𝑚 + 1) ∈ ℝ)
125123, 124syl 17 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ)
126 simpr 477 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ 𝑚)
127123lep1d 10940 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1))
128119, 123, 125, 126, 127letrd 10179 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → (𝐹𝑥) ≤ (𝑚 + 1))
129128iftrued 4085 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) = (𝐹𝑥))
130120, 122, 1293brtr4d 4676 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
131 iffalse 4086 . . . . . . . . 9 (¬ (𝐹𝑥) ≤ 𝑚 → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
132131adantl 482 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = 0)
133116simprd 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
134 0le0 11095 . . . . . . . . . . 11 0 ≤ 0
135 breq2 4648 . . . . . . . . . . . 12 ((𝐹𝑥) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
136 breq2 4648 . . . . . . . . . . . 12 (0 = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) → (0 ≤ 0 ↔ 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
137135, 136ifboth 4115 . . . . . . . . . . 11 ((0 ≤ (𝐹𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
138133, 134, 137sylancl 693 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
139138adantlr 750 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
140139adantr 481 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → 0 ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
141132, 140eqbrtrd 4666 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹𝑥) ≤ 𝑚) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
142130, 141pm2.61dan 831 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
143142ralrimiva 2963 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
1441, 2ifex 4147 . . . . . . 7 if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V
145144a1i 11 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0) ∈ V)
146 eqidd 2621 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
147 eqidd 2621 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
14881, 110, 145, 146, 147ofrfval2 6900 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
149143, 148mpbird 247 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
150 peano2nn 11017 . . . . . 6 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
151150adantl 482 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
152 breq2 4648 . . . . . . . 8 (𝑛 = (𝑚 + 1) → ((𝐹𝑥) ≤ 𝑛 ↔ (𝐹𝑥) ≤ (𝑚 + 1)))
153152ifbid 4099 . . . . . . 7 (𝑛 = (𝑚 + 1) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) = if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0))
154153mpteq2dv 4736 . . . . . 6 (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
15532mptex 6471 . . . . . 6 (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)) ∈ V
156154, 31, 155fvmpt 6269 . . . . 5 ((𝑚 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
157151, 156syl 17 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ (𝑚 + 1), (𝐹𝑥), 0)))
158149, 47, 1573brtr4d 4676 . . 3 ((𝜑𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) ∘𝑟 ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘(𝑚 + 1)))
15964ffvelrnda 6345 . . . 4 ((𝜑𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
16034adantl 482 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)))
161160fveq1d 6180 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
162117leidd 10579 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ (𝐹𝑥))
163 breq1 4647 . . . . . . . . . . . . . 14 ((𝐹𝑥) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → ((𝐹𝑥) ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
164 breq1 4647 . . . . . . . . . . . . . 14 (0 = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) → (0 ≤ (𝐹𝑥) ↔ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
165163, 164ifboth 4115 . . . . . . . . . . . . 13 (((𝐹𝑥) ≤ (𝐹𝑥) ∧ 0 ≤ (𝐹𝑥)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
166162, 133, 165syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
167166adantlr 750 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
168167ralrimiva 2963 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
16932a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ℝ ∈ V)
1701, 2ifex 4147 . . . . . . . . . . . 12 if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V
171170a1i 11 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ∈ V)
17253feqmptd 6236 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
173172adantr 481 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
174169, 171, 118, 146, 173ofrfval2 6900 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥)))
175168, 174mpbird 247 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹)
176171, 111fmptd 6371 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶V)
177 ffn 6032 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)):ℝ⟶V → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) Fn ℝ)
178176, 177syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) Fn ℝ)
17955adantr 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹 Fn ℝ)
180 inidm 3814 . . . . . . . . . 10 (ℝ ∩ ℝ) = ℝ
181 eqidd 2621 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦))
182 eqidd 2621 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) = (𝐹𝑦))
183178, 179, 169, 169, 180, 181, 182ofrfval 6890 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0)) ∘𝑟𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦)))
184175, 183mpbid 222 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
185184r19.21bi 2929 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
186185an32s 845 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))‘𝑦) ≤ (𝐹𝑦))
187161, 186eqbrtrd 4666 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
188187ralrimiva 2963 . . . 4 ((𝜑𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦))
189 breq2 4648 . . . . . 6 (𝑧 = (𝐹𝑦) → ((((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧 ↔ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦)))
190189ralbidv 2983 . . . . 5 (𝑧 = (𝐹𝑦) → (∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧 ↔ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦)))
191190rspcev 3304 . . . 4 (((𝐹𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
192159, 188, 191syl2anc 692 . . 3 ((𝜑𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧)
19328fveq2d 6182 . . . . . . 7 (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
194193cbvmptv 4741 . . . . . 6 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
19534fveq2d 6182 . . . . . . 7 (𝑚 ∈ ℕ → (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
196195mpteq2ia 4731 . . . . . 6 (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))))
197194, 196eqtr4i 2645 . . . . 5 (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
198197rneqi 5341 . . . 4 ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚)))
199198supeq1i 8338 . . 3 sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = sup(ran (𝑚 ∈ ℕ ↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))‘𝑚))), ℝ*, < )
20042, 105, 114, 158, 192, 199itg2mono 23501 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ))
201 eqid 2620 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))
20227, 201, 170fvmpt 6269 . . . . . . . . . . 11 (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
203202adantl 482 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
204166adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) ≤ (𝐹𝑥))
205203, 204eqbrtrd 4666 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
206205ralrimiva 2963 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥))
2073a1i 11 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ V)
208207, 201fmptd 6371 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶V)
209 ffn 6032 . . . . . . . . . 10 ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶V → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
210208, 209syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
211 breq1 4647 . . . . . . . . . 10 (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
212211ralrn 6348 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
213210, 212syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ≤ (𝐹𝑥)))
214206, 213mpbird 247 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥))
215117adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑥) ∈ ℝ)
216 0re 10025 . . . . . . . . . . 11 0 ∈ ℝ
217 ifcl 4121 . . . . . . . . . . 11 (((𝐹𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
218215, 216, 217sylancl 693 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0) ∈ ℝ)
219218, 201fmptd 6371 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶ℝ)
220 frn 6040 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ)
221219, 220syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ)
222 1nn 11016 . . . . . . . . . 10 1 ∈ ℕ
223201, 218dmmptd 6011 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ℕ)
224222, 223syl5eleqr 2706 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
225 n0i 3912 . . . . . . . . . 10 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
226 dm0rn0 5331 . . . . . . . . . . 11 (dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅)
227226necon3bbii 2838 . . . . . . . . . 10 (¬ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
228225, 227sylib 208 . . . . . . . . 9 (1 ∈ dom (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
229224, 228syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅)
230 breq2 4648 . . . . . . . . . . 11 (𝑧 = (𝐹𝑥) → (𝑤𝑧𝑤 ≤ (𝐹𝑥)))
231230ralbidv 2983 . . . . . . . . . 10 (𝑧 = (𝐹𝑥) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧 ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
232231rspcev 3304 . . . . . . . . 9 (((𝐹𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
233117, 214, 232syl2anc 692 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧)
234 suprleub 10974 . . . . . . . 8 (((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) ∧ (𝐹𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
235221, 229, 233, 117, 234syl31anc 1327 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤 ≤ (𝐹𝑥)))
236214, 235mpbird 247 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥))
237 arch 11274 . . . . . . . . 9 ((𝐹𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
238117, 237syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹𝑥) < 𝑚)
239202ad2antrl 763 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0))
240 ltle 10111 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
241117, 48, 240syl2an 494 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑥) < 𝑚 → (𝐹𝑥) ≤ 𝑚))
242241impr 648 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ≤ 𝑚)
243242iftrued 4085 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → if((𝐹𝑥) ≤ 𝑚, (𝐹𝑥), 0) = (𝐹𝑥))
244239, 243eqtrd 2654 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) = (𝐹𝑥))
245210adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ)
246 simprl 793 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → 𝑚 ∈ ℕ)
247 fnfvelrn 6342 . . . . . . . . . 10 (((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
248245, 246, 247syl2anc 692 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
249244, 248eqeltrrd 2700 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹𝑥) < 𝑚)) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
250238, 249rexlimddv 3031 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))
251 suprub 10969 . . . . . . 7 (((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) ∧ (𝐹𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))) → (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
252221, 229, 233, 250, 251syl31anc 1327 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))
253 suprcl 10968 . . . . . . . 8 ((ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0))𝑤𝑧) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ∈ ℝ)
254221, 229, 233, 253syl3anc 1324 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ∈ ℝ)
255254, 117letri3d 10164 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) ≤ (𝐹𝑥) ∧ (𝐹𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))))
256236, 252, 255mpbir2and 956 . . . . 5 ((𝜑𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ) = (𝐹𝑥))
257256mpteq2dva 4735 . . . 4 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
258257, 172eqtr4d 2657 . . 3 (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < )) = 𝐹)
259258fveq2d 6182 . 2 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)), ℝ, < ))) = (∫2𝐹))
260200, 259eqtr3d 2656 1 (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹𝑥) ≤ 𝑛, (𝐹𝑥), 0)))), ℝ*, < ) = (∫2𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cdif 3564  wss 3567  c0 3907  ifcif 4077   class class class wbr 4644  cmpt 4720  ccnv 5103  dom cdm 5104  ran crn 5105  cres 5106  cima 5107   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  𝑟 cofr 6881  supcsup 8331  cr 9920  0cc0 9921  1c1 9922   + caddc 9924  +∞cpnf 10056  *cxr 10058   < clt 10059  cle 10060  cn 11005  (,)cioo 12160  [,)cico 12162  volcvol 23213  MblFncmbf 23364  2citg2 23366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cc 9242  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-disj 4612  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-ofr 6883  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-omul 7550  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-acn 8753  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-rest 16064  df-topgen 16085  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-top 20680  df-topon 20697  df-bases 20731  df-cmp 21171  df-ovol 23214  df-vol 23215  df-mbf 23369  df-itg1 23370  df-itg2 23371
This theorem is referenced by:  itg2cn  23511
  Copyright terms: Public domain W3C validator