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 nfrex 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