Metamath Proof Explorer

Theorem smfsup

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 smfsup.n ⊢ Ⅎ _ n F
smfsup.x ⊢ Ⅎ _ x F
smfsup.m ⊢ φ → M ∈ ℤ
smfsup.z ⊢ Z = ℤ ≥ M
smfsup.s ⊢ φ → S ∈ SAlg
smfsup.f ⊢ φ → F : Z ⟶ SMblFn ⁡ S
smfsup.d ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
smfsup.g ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
Assertion smfsup ⊢ φ → G ∈ SMblFn ⁡ S

Proof

Step Hyp Ref Expression
1 smfsup.n ⊢ Ⅎ _ n F
2 smfsup.x ⊢ Ⅎ _ x F
3 smfsup.m ⊢ φ → M ∈ ℤ
4 smfsup.z ⊢ Z = ℤ ≥ M
5 smfsup.s ⊢ φ → S ∈ SAlg
6 smfsup.f ⊢ φ → F : Z ⟶ SMblFn ⁡ S
7 smfsup.d ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
8 smfsup.g ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
9 nfcv ⊢ Ⅎ _ w ⋂ n ∈ Z dom ⁡ F ⁡ n
10 nfcv ⊢ Ⅎ _ x Z
11 nfcv ⊢ Ⅎ _ x m
12 2 11 nffv ⊢ Ⅎ _ x F ⁡ m
13 12 nfdm ⊢ Ⅎ _ x dom ⁡ F ⁡ m
14 10 13 nfiin ⊢ Ⅎ _ x ⋂ m ∈ Z dom ⁡ F ⁡ m
15 nfv ⊢ Ⅎ w ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
16 nfcv ⊢ Ⅎ _ x ℝ
17 nfcv ⊢ Ⅎ _ x w
18 12 17 nffv ⊢ Ⅎ _ x F ⁡ m ⁡ w
19 nfcv ⊢ Ⅎ _ x ≤
20 nfcv ⊢ Ⅎ _ x z
21 18 19 20 nfbr ⊢ Ⅎ x F ⁡ m ⁡ w ≤ z
22 10 21 nfralw ⊢ Ⅎ x ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
23 16 22 nfrexw ⊢ Ⅎ x ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
24 nfcv ⊢ Ⅎ _ m dom ⁡ F ⁡ n
25 nfcv ⊢ Ⅎ _ n m
26 1 25 nffv ⊢ Ⅎ _ n F ⁡ m
27 26 nfdm ⊢ Ⅎ _ n dom ⁡ F ⁡ m
28 fveq2 ⊢ n = m → F ⁡ n = F ⁡ m
29 28 dmeqd ⊢ n = m → dom ⁡ F ⁡ n = dom ⁡ F ⁡ m
30 24 27 29 cbviin ⊢ ⋂ n ∈ Z dom ⁡ F ⁡ n = ⋂ m ∈ Z dom ⁡ F ⁡ m
31 30 a1i ⊢ x = w → ⋂ n ∈ Z dom ⁡ F ⁡ n = ⋂ m ∈ Z dom ⁡ F ⁡ m
32 fveq2 ⊢ x = w → F ⁡ n ⁡ x = F ⁡ n ⁡ w
33 32 breq1d ⊢ x = w → F ⁡ n ⁡ x ≤ y ↔ F ⁡ n ⁡ w ≤ y
34 33 ralbidv ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∀ n ∈ Z F ⁡ n ⁡ w ≤ y
35 nfv ⊢ Ⅎ m F ⁡ n ⁡ w ≤ y
36 nfcv ⊢ Ⅎ _ n w
37 26 36 nffv ⊢ Ⅎ _ n F ⁡ m ⁡ w
38 nfcv ⊢ Ⅎ _ n ≤
39 nfcv ⊢ Ⅎ _ n y
40 37 38 39 nfbr ⊢ Ⅎ n F ⁡ m ⁡ w ≤ y
41 28 fveq1d ⊢ n = m → F ⁡ n ⁡ w = F ⁡ m ⁡ w
42 41 breq1d ⊢ n = m → F ⁡ n ⁡ w ≤ y ↔ F ⁡ m ⁡ w ≤ y
43 35 40 42 cbvralw ⊢ ∀ n ∈ Z F ⁡ n ⁡ w ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
44 43 a1i ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ w ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
45 34 44 bitrd ⊢ x = w → ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
46 45 rexbidv ⊢ x = w → ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y
47 breq2 ⊢ y = z → F ⁡ m ⁡ w ≤ y ↔ F ⁡ m ⁡ w ≤ z
48 47 ralbidv ⊢ y = z → ∀ m ∈ Z F ⁡ m ⁡ w ≤ y ↔ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
49 48 cbvrexvw ⊢ ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y ↔ ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
50 49 a1i ⊢ x = w → ∃ y ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ y ↔ ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
51 46 50 bitrd ⊢ x = w → ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y ↔ ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
52 9 14 15 23 31 51 cbvrabcsfw ⊢ x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y = w ∈ ⋂ m ∈ Z dom ⁡ F ⁡ m | ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
53 7 52 eqtri ⊢ D = w ∈ ⋂ m ∈ Z dom ⁡ F ⁡ m | ∃ z ∈ ℝ ∀ m ∈ Z F ⁡ m ⁡ w ≤ z
54 nfrab1 ⊢ Ⅎ _ x x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
55 7 54 nfcxfr ⊢ Ⅎ _ x D
56 nfcv ⊢ Ⅎ _ w D
57 nfcv ⊢ Ⅎ _ w sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
58 10 18 nfmpt ⊢ Ⅎ _ x m ∈ Z ⟼ F ⁡ m ⁡ w
59 58 nfrn ⊢ Ⅎ _ x ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w
60 nfcv ⊢ Ⅎ _ x <
61 59 16 60 nfsup ⊢ Ⅎ _ x sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
62 32 mpteq2dv ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ x = n ∈ Z ⟼ F ⁡ n ⁡ w
63 nfcv ⊢ Ⅎ _ m F ⁡ n ⁡ w
64 63 37 41 cbvmpt ⊢ n ∈ Z ⟼ F ⁡ n ⁡ w = m ∈ Z ⟼ F ⁡ m ⁡ w
65 64 a1i ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ w = m ∈ Z ⟼ F ⁡ m ⁡ w
66 62 65 eqtrd ⊢ x = w → n ∈ Z ⟼ F ⁡ n ⁡ x = m ∈ Z ⟼ F ⁡ m ⁡ w
67 66 rneqd ⊢ x = w → ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x = ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w
68 67 supeq1d ⊢ x = w → sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < = sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
69 55 56 57 61 68 cbvmptf ⊢ x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < = w ∈ D ⟼ sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
70 8 69 eqtri ⊢ G = w ∈ D ⟼ sup ran ⁡ m ∈ Z ⟼ F ⁡ m ⁡ w ℝ <
71 3 4 5 6 53 70 smfsuplem3 ⊢ φ → G ∈ SMblFn ⁡ S