Step | Hyp | Ref
| Expression |
1 | | iftrue 4492 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) = (𝐹‘𝑦)) |
2 | 1 | mpteq2ia 5208 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0)) = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦)) |
3 | | mbfi1flim.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
4 | 3 | feqmptd 6910 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦))) |
5 | | mbfi1flim.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ MblFn) |
6 | 4, 5 | eqeltrrd 2839 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦)) ∈ MblFn) |
7 | 2, 6 | eqeltrid 2842 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0)) ∈ MblFn) |
8 | | fvex 6855 |
. . . . . . . 8
⊢ (𝐹‘𝑦) ∈ V |
9 | | c0ex 11149 |
. . . . . . . 8
⊢ 0 ∈
V |
10 | 8, 9 | ifex 4536 |
. . . . . . 7
⊢ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) ∈ V |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) ∈ V) |
12 | 7, 11 | mbfdm2 25001 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ dom vol) |
13 | | mblss 24895 |
. . . . 5
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
15 | | rembl 24904 |
. . . . 5
⊢ ℝ
∈ dom vol |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈ dom
vol) |
17 | | eldifn 4087 |
. . . . . 6
⊢ (𝑦 ∈ (ℝ ∖ 𝐴) → ¬ 𝑦 ∈ 𝐴) |
18 | 17 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑦 ∈ 𝐴) |
19 | 18 | iffalsed 4497 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℝ ∖ 𝐴)) → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) = 0) |
20 | 14, 16, 11, 19, 7 | mbfss 25010 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0)) ∈ MblFn) |
21 | 3 | ffvelcdmda 7035 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℝ) |
22 | | 0red 11158 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑦 ∈ 𝐴) → 0 ∈ ℝ) |
23 | 21, 22 | ifclda 4521 |
. . . . 5
⊢ (𝜑 → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) ∈ ℝ) |
24 | 23 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) ∈ ℝ) |
25 | 24 | fmpttd 7063 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦),
0)):ℝ⟶ℝ) |
26 | 20, 25 | mbfi1flimlem 25087 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥))) |
27 | | ssralv 4010 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) → ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥))) |
28 | 14, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) → ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥))) |
29 | 14 | sselda 3944 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
30 | | eleq1w 2820 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
31 | | fveq2 6842 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
32 | 30, 31 | ifbieq1d 4510 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0) = if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) |
33 | | eqid 2736 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0)) |
34 | | fvex 6855 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
35 | 34, 9 | ifex 4536 |
. . . . . . . . . 10
⊢ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) ∈ V |
36 | 32, 33, 35 | fvmpt 6948 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) = if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) |
37 | 29, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) = if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) |
38 | | iftrue 4492 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
39 | 38 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
40 | 37, 39 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) = (𝐹‘𝑥)) |
41 | 40 | breq2d 5117 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
42 | 41 | ralbidva 3172 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
43 | 28, 42 | sylibd 238 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥) → ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
44 | 43 | anim2d 612 |
. . 3
⊢ (𝜑 → ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥)) → (𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
45 | 44 | eximdv 1920 |
. 2
⊢ (𝜑 → (∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ ℝ
(𝑛 ∈ ℕ ↦
((𝑔‘𝑛)‘𝑥)) ⇝ ((𝑦 ∈ ℝ ↦ if(𝑦 ∈ 𝐴, (𝐹‘𝑦), 0))‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
46 | 26, 45 | mpd 15 |
1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |