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 eqidd φ n Z x A B = n Z x A B
12 11 8 fvmpt2d φ n Z n Z x A B n = x A B
13 12 dmeqd φ n Z dom n Z x A B n = dom x A B
14 nfcv _ x Z
15 14 nfcri x n Z
16 2 15 nfan x φ n Z
17 eqid x A B = x A B
18 7 3expa φ n Z x A B V
19 16 17 18 dmmptdf φ n Z dom x A B = A
20 13 19 eqtr2d φ n Z A = dom n Z x A B n
21 1 20 iineq2d φ n Z A = n Z dom n Z x A B n
22 nfcv _ x n Z A
23 nfmpt1 _ x x A B
24 14 23 nfmpt _ x n Z x A B
25 nfcv _ x n
26 24 25 nffv _ x n Z x A B n
27 26 nfdm _ x dom n Z x A B n
28 14 27 nfiin _ x n Z dom n Z x A B n
29 22 28 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
30 21 29 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
31 nfv y x n Z dom n Z x A B n
32 3 31 nfan y φ x n Z dom n Z x A B n
33 nfii1 _ n n Z dom n Z x A B n
34 33 nfcri n x n Z dom n Z x A B n
35 1 34 nfan n φ x n Z dom n Z x A B n
36 simpll φ x n Z dom n Z x A B n n Z φ
37 simpr φ x n Z dom n Z x A B n n Z n Z
38 eliinid x n Z dom n Z x A B n n Z x dom n Z x A B n
39 38 adantll φ x n Z dom n Z x A B n n Z x dom n Z x A B n
40 13 19 eqtrd φ n Z dom n Z x A B n = A
41 40 adantlr φ x n Z dom n Z x A B n n Z dom n Z x A B n = A
42 39 41 eleqtrd φ x n Z dom n Z x A B n n Z x A
43 12 fveq1d φ n Z n Z x A B n x = x A B x
44 43 3adant3 φ n Z x A n Z x A B n x = x A B x
45 simp3 φ n Z x A x A
46 fvmpt4 x A B V x A B x = B
47 45 7 46 syl2anc φ n Z x A x A B x = B
48 44 47 eqtr2d φ n Z x A B = n Z x A B n x
49 48 breq1d φ n Z x A B y n Z x A B n x y
50 36 37 42 49 syl3anc φ x n Z dom n Z x A B n n Z B y n Z x A B n x y
51 35 50 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
52 32 51 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
53 2 52 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
54 30 53 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
55 9 54 syl5eq φ D = x n Z dom n Z x A B n | y n Z n Z x A B n x y
56 nfcv _ n
57 nfra1 n n Z B y
58 56 57 nfrex n y n Z B y
59 nfii1 _ n n Z A
60 58 59 nfrabw _ n x n Z A | y n Z B y
61 9 60 nfcxfr _ n D
62 61 nfcri n x D
63 1 62 nfan n φ x D
64 simpll φ x D n Z φ
65 simpr φ x D n Z n Z
66 rabidim1 x x n Z A | y n Z B y x n Z A
67 66 9 eleq2s x D x n Z A
68 eliinid x n Z A n Z x A
69 67 68 sylan x D n Z x A
70 69 adantll φ x D n Z x A
71 64 65 70 48 syl3anc φ x D n Z B = n Z x A B n x
72 63 71 mpteq2da φ x D n Z B = n Z n Z x A B n x
73 72 rneqd φ x D ran n Z B = ran n Z n Z x A B n x
74 73 supeq1d φ x D sup ran n Z B < = sup ran n Z n Z x A B n x <
75 2 55 74 mpteq12da φ 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 <
76 10 75 syl5eq φ 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 <
77 nfmpt1 _ n n Z x A B
78 1 8 fmptd2f φ n Z x A B : Z SMblFn S
79 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
80 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 <
81 77 24 4 5 6 78 79 80 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
82 76 81 eqeltrd φ G SMblFn S