Metamath Proof Explorer


Theorem smfsupmpt

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 smfsupmpt.n n φ
smfsupmpt.x x φ
smfsupmpt.y y φ
smfsupmpt.m φ M
smfsupmpt.z Z = M
smfsupmpt.s φ S SAlg
smfsupmpt.b φ n Z x A B V
smfsupmpt.f φ n Z x A B SMblFn S
smfsupmpt.d D = x n Z A | y n Z B y
smfsupmpt.g G = x D sup ran n Z B <
Assertion smfsupmpt φ G SMblFn S

Proof

Step Hyp Ref Expression
1 smfsupmpt.n n φ
2 smfsupmpt.x x φ
3 smfsupmpt.y y φ
4 smfsupmpt.m φ M
5 smfsupmpt.z Z = M
6 smfsupmpt.s φ S SAlg
7 smfsupmpt.b φ n Z x A B V
8 smfsupmpt.f φ n Z x A B SMblFn S
9 smfsupmpt.d D = x n Z A | y n Z B y
10 smfsupmpt.g G = x D sup ran n Z B <
11 10 a1i φ G = x D sup ran n Z B <
12 9 a1i φ D = x n Z A | y n Z B y
13 eqidd φ n Z x A B = n Z x A B
14 13 8 fvmpt2d φ n Z n Z x A B n = x A B
15 14 dmeqd φ n Z dom n Z x A B n = dom x A B
16 nfcv _ x n
17 nfcv _ x Z
18 16 17 nfel x n Z
19 2 18 nfan x φ n Z
20 eqid x A B = x A B
21 6 adantr φ n Z S SAlg
22 7 3expa φ n Z x A B V
23 19 21 22 8 smffmpt φ n Z x A B : A
24 23 fvmptelrn φ n Z x A B
25 19 20 24 dmmptdf φ n Z dom x A B = A
26 eqidd φ n Z A = A
27 15 25 26 3eqtrrd φ n Z A = dom n Z x A B n
28 1 27 iineq2d φ n Z A = n Z dom n Z x A B n
29 nfcv _ x n Z A
30 nfmpt1 _ x x A B
31 17 30 nfmpt _ x n Z x A B
32 31 16 nffv _ x n Z x A B n
33 32 nfdm _ x dom n Z x A B n
34 17 33 nfiin _ x n Z dom n Z x A B n
35 29 34 rabeqf n Z A = n Z dom n Z x A B n x n Z A | y n Z B y = x n Z dom n Z x A B n | y n Z B y
36 28 35 syl φ x n Z A | y n Z B y = x n Z dom n Z x A B n | y n Z B y
37 nfv y x n Z dom n Z x A B n
38 3 37 nfan y φ x n Z dom n Z x A B n
39 nfcv _ n x
40 nfii1 _ n n Z dom n Z x A B n
41 39 40 nfel n x n Z dom n Z x A B n
42 1 41 nfan n φ x n Z dom n Z x A B n
43 simpll φ x n Z dom n Z x A B n n Z φ
44 simpr φ x n Z dom n Z x A B n n Z n Z
45 eliinid x n Z dom n Z x A B n n Z x dom n Z x A B n
46 45 adantll φ x n Z dom n Z x A B n n Z x dom n Z x A B n
47 27 eqcomd φ n Z dom n Z x A B n = A
48 47 adantlr φ x n Z dom n Z x A B n n Z dom n Z x A B n = A
49 46 48 eleqtrd φ x n Z dom n Z x A B n n Z x A
50 14 fveq1d φ n Z n Z x A B n x = x A B x
51 50 3adant3 φ n Z x A n Z x A B n x = x A B x
52 simp3 φ n Z x A x A
53 20 fvmpt2 x A B V x A B x = B
54 52 7 53 syl2anc φ n Z x A x A B x = B
55 51 54 eqtr2d φ n Z x A B = n Z x A B n x
56 55 breq1d φ n Z x A B y n Z x A B n x y
57 43 44 49 56 syl3anc φ x n Z dom n Z x A B n n Z B y n Z x A B n x y
58 42 57 ralbida φ x n Z dom n Z x A B n n Z B y n Z n Z x A B n x y
59 38 58 rexbid φ x n Z dom n Z x A B n y n Z B y y n Z n Z x A B n x y
60 2 59 rabbida φ x n Z dom n Z x A B n | y n Z B y = x n Z dom n Z x A B n | y n Z n Z x A B n x y
61 36 60 eqtrd φ x n Z A | y n Z B y = x n Z dom n Z x A B n | y n Z n Z x A B n x y
62 12 61 eqtrd φ D = x n Z dom n Z x A B n | y n Z n Z x A B n x y
63 2 62 alrimi φ x D = x n Z dom n Z x A B n | y n Z n Z x A B n x y
64 nfcv _ n
65 nfra1 n n Z B y
66 64 65 nfrex n y n Z B y
67 nfii1 _ n n Z A
68 66 67 nfrabw _ n x n Z A | y n Z B y
69 9 68 nfcxfr _ n D
70 39 69 nfel n x D
71 1 70 nfan n φ x D
72 simpll φ x D n Z φ
73 simpr φ x D n Z n Z
74 9 eleq2i x D x x n Z A | y n Z B y
75 74 biimpi x D x x n Z A | y n Z B y
76 rabidim1 x x n Z A | y n Z B y x n Z A
77 75 76 syl x D x n Z A
78 77 adantr x D n Z x n Z A
79 simpr x D n Z n Z
80 eliinid x n Z A n Z x A
81 78 79 80 syl2anc x D n Z x A
82 81 adantll φ x D n Z x A
83 55 idi φ n Z x A B = n Z x A B n x
84 72 73 82 83 syl3anc φ x D n Z B = n Z x A B n x
85 71 84 mpteq2da φ x D n Z B = n Z n Z x A B n x
86 85 rneqd φ x D ran n Z B = ran n Z n Z x A B n x
87 86 supeq1d φ x D sup ran n Z B < = sup ran n Z n Z x A B n x <
88 87 ex φ x D sup ran n Z B < = sup ran n Z n Z x A B n x <
89 2 88 ralrimi φ x D sup ran n Z B < = sup ran n Z n Z x A B n x <
90 mpteq12f x D = x n Z dom n Z x A B n | y n Z n Z x A B n x y x D sup ran n Z B < = sup ran n Z n Z x A B n x < x D sup ran n Z B < = x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x <
91 63 89 90 syl2anc φ x D sup ran n Z B < = x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x <
92 11 91 eqtrd φ G = x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x <
93 nfmpt1 _ n n Z x A B
94 eqid n Z x A B = n Z x A B
95 1 8 94 fmptdf φ n Z x A B : Z SMblFn S
96 eqid x n Z dom n Z x A B n | y n Z n Z x A B n x y = x n Z dom n Z x A B n | y n Z n Z x A B n x y
97 eqid x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x < = x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x <
98 93 31 4 5 6 95 96 97 smfsup φ x x n Z dom n Z x A B n | y n Z n Z x A B n x y sup ran n Z n Z x A B n x < SMblFn S
99 92 98 eqeltrd φ G SMblFn S