Metamath Proof Explorer

Theorem smfsuplem2

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfsuplem2.m ⊢ φ → M ∈ ℤ
smfsuplem2.z ⊢ Z = ℤ ≥ M
smfsuplem2.s ⊢ φ → S ∈ SAlg
smfsuplem2.f ⊢ φ → F : Z ⟶ SMblFn ⁡ S
smfsuplem2.d ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
smfsuplem2.g ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
smfsuplem2.8 ⊢ φ → A ∈ ℝ
Assertion smfsuplem2 ⊢ φ → G -1 −∞ A ∈ S ↾ 𝑡 D

Proof

Step Hyp Ref Expression
1 smfsuplem2.m ⊢ φ → M ∈ ℤ
2 smfsuplem2.z ⊢ Z = ℤ ≥ M
3 smfsuplem2.s ⊢ φ → S ∈ SAlg
4 smfsuplem2.f ⊢ φ → F : Z ⟶ SMblFn ⁡ S
5 smfsuplem2.d ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
6 smfsuplem2.g ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
7 smfsuplem2.8 ⊢ φ → A ∈ ℝ
8 nfcv ⊢ Ⅎ _ n F
9 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
10 eqid ⊢ SalGen ⁡ topGen ⁡ ran ⁡ . = SalGen ⁡ topGen ⁡ ran ⁡ .
11 mnfxr ⊢ −∞ ∈ ℝ *
12 11 a1i ⊢ φ → −∞ ∈ ℝ *
13 12 7 9 10 iocborel ⊢ φ → −∞ A ∈ SalGen ⁡ topGen ⁡ ran ⁡ .
14 8 2 3 4 9 10 13 smfpimcc ⊢ φ → ∃ h h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n
15 1 adantr ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → M ∈ ℤ
16 3 adantr ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → S ∈ SAlg
17 4 adantr ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → F : Z ⟶ SMblFn ⁡ S
18 fveq2 ⊢ n = m → F ⁡ n = F ⁡ m
19 18 dmeqd ⊢ n = m → dom ⁡ F ⁡ n = dom ⁡ F ⁡ m
20 19 cbviinv ⊢ ⋂ n ∈ Z dom ⁡ F ⁡ n = ⋂ m ∈ Z dom ⁡ F ⁡ m
21 20 a1i ⊢ x = w → ⋂ n ∈ Z dom ⁡ F ⁡ n = ⋂ m ∈ Z dom ⁡ F ⁡ m
22 fveq2 ⊢ x = w → F ⁡ n ⁡ x = F ⁡ n ⁡ w
23 22 breq1d ⊢ x = w → F ⁡ n ⁡ x ≤ y ↔ F ⁡ n ⁡ w ≤ y
24 23 ralbidv ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∀ n ∈ Z F ⁡ n ⁡ w ≤ y
25 18 fveq1d ⊢ n = m → F ⁡ n ⁡ w = F ⁡ m ⁡ w
26 25 breq1d ⊢ n = m → F ⁡ n ⁡ w ≤ y ↔ F ⁡ m ⁡ w ≤ y
27 26 cbvralvw ⊢ ∀ n ∈ Z F ⁡ n ⁡ w ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
28 27 a1i ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ w ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
29 24 28 bitrd ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
30 29 rexbidv ⊢ x = w → ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
31 21 30 cbvrabv2w ⊢ x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y = w ∈ ⋂ m ∈ Z dom ⁡ F ⁡ m | ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
32 5 31 eqtri ⊢ D = w ∈ ⋂ m ∈ Z dom ⁡ F ⁡ m | ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
33 22 mpteq2dv ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ x = n ∈ Z ⟼ F ⁡ n ⁡ w
34 25 cbvmptv ⊢ n ∈ Z ⟼ F ⁡ n ⁡ w = m ∈ Z ⟼ F ⁡ m ⁡ w
35 34 a1i ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ w = m ∈ Z ⟼ F ⁡ m ⁡ w
36 33 35 eqtrd ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ x = m ∈ Z ⟼ F ⁡ m ⁡ w
37 36 rneqd ⊢ x = w → ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x = ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w
38 37 supeq1d ⊢ x = w → sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < = sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
39 38 cbvmptv ⊢ x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < = w ∈ D ⟼ sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
40 6 39 eqtri ⊢ G = w ∈ D ⟼ sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
41 7 adantr ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → A ∈ ℝ
42 simprl ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → h : Z ⟶ S
43 simplrr ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n ∧ m ∈ Z → ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n
44 18 cnveqd ⊢ n = m → F ⁡ n -1 = F ⁡ m -1
45 44 imaeq1d ⊢ n = m → F ⁡ n -1 −∞ A = F ⁡ m -1 −∞ A
46 fveq2 ⊢ n = m → h ⁡ n = h ⁡ m
47 46 19 ineq12d ⊢ n = m → h ⁡ n ∩ dom ⁡ F ⁡ n = h ⁡ m ∩ dom ⁡ F ⁡ m
48 45 47 eqeq12d ⊢ n = m → F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n ↔ F ⁡ m -1 −∞ A = h ⁡ m ∩ dom ⁡ F ⁡ m
49 48 rspccva ⊢ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n ∧ m ∈ Z → F ⁡ m -1 −∞ A = h ⁡ m ∩ dom ⁡ F ⁡ m
50 43 49 sylancom ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n ∧ m ∈ Z → F ⁡ m -1 −∞ A = h ⁡ m ∩ dom ⁡ F ⁡ m
51 15 2 16 17 32 40 41 42 50 smfsuplem1 ⊢ φ ∧ h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → G -1 −∞ A ∈ S ↾ 𝑡 D
52 51 ex ⊢ φ → h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → G -1 −∞ A ∈ S ↾ 𝑡 D
53 52 exlimdv ⊢ φ → ∃ h h : Z ⟶ S ∧ ∀ n ∈ Z F ⁡ n -1 −∞ A = h ⁡ n ∩ dom ⁡ F ⁡ n → G -1 −∞ A ∈ S ↾ 𝑡 D
54 14 53 mpd ⊢ φ → G -1 −∞ A ∈ S ↾ 𝑡 D