Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | smflimlem5.1 | ⊢ ( 𝜑 → 𝑀 ∈ ℤ ) | |
| smflimlem5.2 | ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) | ||
| smflimlem5.3 | ⊢ ( 𝜑 → 𝑆 ∈ SAlg ) | ||
| smflimlem5.4 | ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) | ||
| smflimlem5.5 | ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } | ||
| smflimlem5.6 | ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) | ||
| smflimlem5.7 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | ||
| smflimlem5.8 | ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) | ||
| smflimlem5.9 | ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) | ||
| smflimlem5.10 | ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) | ||
| smflimlem5.11 | ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) | ||
| Assertion | smflimlem5 | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | smflimlem5.1 | ⊢ ( 𝜑 → 𝑀 ∈ ℤ ) | |
| 2 | smflimlem5.2 | ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) | |
| 3 | smflimlem5.3 | ⊢ ( 𝜑 → 𝑆 ∈ SAlg ) | |
| 4 | smflimlem5.4 | ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) | |
| 5 | smflimlem5.5 | ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } | |
| 6 | smflimlem5.6 | ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) | |
| 7 | smflimlem5.7 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
| 8 | smflimlem5.8 | ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) | |
| 9 | smflimlem5.9 | ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) | |
| 10 | smflimlem5.10 | ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) | |
| 11 | smflimlem5.11 | ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) | |
| 12 | 2 3 4 5 6 7 8 9 10 11 | smflimlem2 | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) ) |
| 13 | 1 2 3 4 5 6 7 8 9 10 11 | smflimlem4 | ⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ⊆ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ) |
| 14 | 12 13 | eqssd | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } = ( 𝐷 ∩ 𝐼 ) ) |
| 15 | 2 3 5 8 9 10 11 | smflimlem1 | ⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ∈ ( 𝑆 ↾t 𝐷 ) ) |
| 16 | 14 15 | eqeltrd | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) ) |