Metamath Proof Explorer

Theorem itg2cnlem1

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
Assertion itg2cnlem1 ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) = ( ∫2 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
2 itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
3 itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
4 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
5 c0ex ⊢ 0 ∈ V
6 4 5 ifex ⊢ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
7 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
8 7 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
9 6 8 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
10 9 mpteq2dv ⊢ ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
11 10 rneqd ⊢ ( 𝑥 ∈ ℝ → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) = ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
12 11 supeq1d ⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) )
13 12 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) )
14 nfcv ⊢ Ⅎ 𝑦 sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) , ℝ , < )
15 nfcv ⊢ Ⅎ 𝑥 ℕ
16 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
17 15 16 nfmpt ⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
18 nfcv ⊢ Ⅎ 𝑥 𝑚
19 17 18 nffv ⊢ Ⅎ 𝑥 ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 )
20 nfcv ⊢ Ⅎ 𝑥 𝑦
21 19 20 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 )
22 15 21 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) )
23 22 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) )
24 nfcv ⊢ Ⅎ 𝑥 ℝ
25 nfcv ⊢ Ⅎ 𝑥 <
26 23 24 25 nfsup ⊢ Ⅎ 𝑥 sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < )
27 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
28 27 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ) )
29 breq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
30 29 ifbid ⊢ ( 𝑛 = 𝑚 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
31 30 mpteq2dv ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
32 31 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
33 32 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
34 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
35 reex ⊢ ℝ ∈ V
36 35 mptex ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ V
37 31 34 36 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
38 37 fveq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
39 38 mpteq2ia ⊢ ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
40 33 39 eqtr4i ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) )
41 28 40 eqtrdi ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) )
42 41 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) )
43 42 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
44 14 26 43 cbvmpt ⊢ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
45 13 44 eqtr3i ⊢ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
46 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
47 46 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
48 47 46 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
49 48 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
50 37 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
51 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
52 51 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → 𝑚 ∈ ℝ )
53 52 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → 𝑚 ∈ ℝ* )
54 elioopnf ⊢ ( 𝑚 ∈ ℝ* → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑚 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) ) )
55 53 54 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑚 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) ) )
56 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
57 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → 𝐹 Fn ℝ )
59 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑚 (,) +∞ ) ) ) )
60 58 59 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑚 (,) +∞ ) ) ) )
61 56 60 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑚 (,) +∞ ) ) )
62 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
63 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
64 1 62 63 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 : ℝ ⟶ ℝ )
66 65 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
67 66 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑚 < ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) ) )
68 55 61 67 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ↔ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) )
69 68 notbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ¬ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ↔ ¬ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) )
70 eldif ⊢ ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
71 70 baib ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↔ ¬ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↔ ¬ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
73 66 52 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ↔ ¬ 𝑚 < ( 𝐹 ‘ 𝑦 ) ) )
74 69 72 73 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
75 74 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) = if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) )
76 75 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑦 ) , 0 ) ) )
77 49 50 76 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) = ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) )
78 difss ⊢ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ⊆ ℝ
79 78 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ⊆ ℝ )
80 rembl ⊢ ℝ ∈ dom vol
81 80 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ℝ ∈ dom vol )
82 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
83 82 5 ifex ⊢ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ V
84 83 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) → if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ∈ V )
85 eldifn ⊢ ( 𝑦 ∈ ( ℝ ∖ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) → ¬ 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
86 85 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ( ℝ ∖ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) ) → ¬ 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
87 86 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ( ℝ ∖ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) ) → if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) = 0 )
88 iftrue ⊢ ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) → if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) = ( 𝐹 ‘ 𝑦 ) )
89 88 mpteq2ia ⊢ ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) )
90 resmpt ⊢ ( ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) = ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
91 78 90 ax-mp ⊢ ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) = ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) )
92 89 91 eqtr4i ⊢ ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) )
93 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
94 93 2 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
95 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ∈ dom vol )
96 2 64 95 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ∈ dom vol )
97 cmmbl ⊢ ( ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ∈ dom vol → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ∈ dom vol )
98 96 97 syl ⊢ ( 𝜑 → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ∈ dom vol )
99 mbfres ⊢ ( ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ∧ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ∈ dom vol ) → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) ∈ MblFn )
100 94 98 99 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ) ∈ MblFn )
101 92 100 eqeltrid ⊢ ( 𝜑 → ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
103 79 81 84 87 102 mbfss ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑚 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
104 77 103 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ∈ MblFn )
105 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
106 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
107 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ∧ 0 ∈ ( 0 [,) +∞ ) ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,) +∞ ) )
108 105 106 107 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,) +∞ ) )
109 108 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,) +∞ ) )
110 50 109 fmpt3d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
111 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
112 105 111 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
113 112 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
114 113 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
115 114 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
116 115 leidd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
117 iftrue ⊢ ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
118 117 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
119 51 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → 𝑚 ∈ ℝ )
120 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
121 119 120 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → ( 𝑚 + 1 ) ∈ ℝ )
122 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 )
123 119 lep1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → 𝑚 ≤ ( 𝑚 + 1 ) )
124 115 119 121 122 123 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) )
125 124 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
126 116 118 125 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
127 iffalse ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
128 127 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
129 112 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
130 0le0 ⊢ 0 ≤ 0
131 breq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
132 breq2 ⊢ ( 0 = if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
133 131 132 ifboth ⊢ ( ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ 0 ) → 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
134 129 130 133 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
135 134 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → 0 ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
137 128 136 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
138 126 137 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
139 138 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
140 4 5 ifex ⊢ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
141 140 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V )
142 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
143 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
144 81 109 141 142 143 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
145 139 144 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
146 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
148 breq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) ) )
149 148 ifbid ⊢ ( 𝑛 = ( 𝑚 + 1 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
150 149 mpteq2dv ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
151 35 mptex ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ V
152 150 34 151 fvmpt ⊢ ( ( 𝑚 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
153 147 152 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝑚 + 1 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
154 145 50 153 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ∘r ≤ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ ( 𝑚 + 1 ) ) )
155 64 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
156 37 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
157 156 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
158 113 leidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
159 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
160 breq1 ⊢ ( 0 = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
161 159 160 ifboth ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
162 158 129 161 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
163 162 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
164 163 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
165 35 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ℝ ∈ V )
166 4 5 ifex ⊢ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
167 166 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V )
168 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
170 165 167 114 142 169 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
171 164 170 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 )
172 167 fmpttd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ V )
173 172 ffnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ )
174 57 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 Fn ℝ )
175 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
176 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) )
177 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
178 173 174 165 165 175 176 177 ofrfval ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
179 171 178 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
180 179 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
181 180 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
182 157 181 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
183 182 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑚 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
184 brralrspcev ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ∀ 𝑚 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
185 155 183 184 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
186 31 fveq2d ⊢ ( 𝑛 = 𝑚 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
187 186 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
188 37 fveq2d ⊢ ( 𝑚 ∈ ℕ → ( ∫2 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
189 188 mpteq2ia ⊢ ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
190 187 189 eqtr4i ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ) )
191 190 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ) )
192 191 supeq1i ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑚 ) ) ) , ℝ* , < )
193 45 104 110 154 185 192 itg2mono ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) )
194 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
195 30 194 166 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
196 195 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
197 162 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
198 196 197 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ≤ ( 𝐹 ‘ 𝑥 ) )
199 198 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ≤ ( 𝐹 ‘ 𝑥 ) )
200 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V )
201 200 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℕ ⟶ V )
202 201 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℕ )
203 breq1 ⊢ ( 𝑤 = ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) → ( 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
204 203 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℕ → ( ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
205 202 204 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
206 199 205 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) )
207 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
208 0re ⊢ 0 ∈ ℝ
209 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
210 207 208 209 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
211 210 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℕ ⟶ ℝ )
212 211 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ⊆ ℝ )
213 1nn ⊢ 1 ∈ ℕ
214 194 210 dmmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ℕ )
215 213 214 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
216 n0i ⊢ ( 1 ∈ dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) → ¬ dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ∅ )
217 dm0rn0 ⊢ ( dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ∅ )
218 217 necon3bbii ⊢ ( ¬ dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ≠ ∅ )
219 216 218 sylib ⊢ ( 1 ∈ dom ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) → ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ≠ ∅ )
220 215 219 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ≠ ∅ )
221 brralrspcev ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ 𝑧 )
222 113 206 221 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ 𝑧 )
223 suprleub ⊢ ( ( ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ 𝑧 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ) )
224 212 220 222 113 223 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) 𝑤 ≤ ( 𝐹 ‘ 𝑥 ) ) )
225 206 224 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ≤ ( 𝐹 ‘ 𝑥 ) )
226 arch ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑥 ) < 𝑚 )
227 113 226 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑥 ) < 𝑚 )
228 195 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
229 ltle ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) < 𝑚 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
230 113 51 229 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) < 𝑚 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
231 230 impr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 )
232 231 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
233 228 232 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑥 ) )
234 202 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℕ )
235 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → 𝑚 ∈ ℕ )
236 fnfvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℕ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
237 234 235 236 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ‘ 𝑚 ) ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
238 233 237 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑚 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
239 227 238 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
240 212 220 222 239 suprubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) )
241 212 220 222 suprcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ∈ ℝ )
242 241 113 letri3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) = ( 𝐹 ‘ 𝑥 ) ↔ ( sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) ) )
243 225 240 242 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) = ( 𝐹 ‘ 𝑥 ) )
244 243 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
245 244 168 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) = 𝐹 )
246 245 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) , ℝ , < ) ) ) = ( ∫2 ‘ 𝐹 ) )
247 193 246 eqtr3d ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑛 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) , ℝ* , < ) = ( ∫2 ‘ 𝐹 ) )