Metamath Proof Explorer


Theorem smfinfmpt

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

Ref Expression
Hypotheses smfinfmpt.n n φ
smfinfmpt.x x φ
smfinfmpt.y y φ
smfinfmpt.m φ M
smfinfmpt.z Z = M
smfinfmpt.s φ S SAlg
smfinfmpt.b φ n Z x A B V
smfinfmpt.f φ n Z x A B SMblFn S
smfinfmpt.d D = x n Z A | y n Z y B
smfinfmpt.g G = x D sup ran n Z B <
Assertion smfinfmpt φ G SMblFn S

Proof

Step Hyp Ref Expression
1 smfinfmpt.n n φ
2 smfinfmpt.x x φ
3 smfinfmpt.y y φ
4 smfinfmpt.m φ M
5 smfinfmpt.z Z = M
6 smfinfmpt.s φ S SAlg
7 smfinfmpt.b φ n Z x A B V
8 smfinfmpt.f φ n Z x A B SMblFn S
9 smfinfmpt.d D = x n Z A | y n Z y B
10 smfinfmpt.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 y B
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 y B = x n Z dom n Z x A B n | y n Z y B
36 28 35 syl φ x n Z A | y n Z y B = x n Z dom n Z x A B n | y n Z y B
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 breq2d φ n Z x A y B y n Z x A B n x
57 43 44 49 56 syl3anc φ x n Z dom n Z x A B n n Z y B y n Z x A B n x
58 42 57 ralbida φ x n Z dom n Z x A B n n Z y B n Z y n Z x A B n x
59 38 58 rexbid φ x n Z dom n Z x A B n y n Z y B y n Z y n Z x A B n x
60 2 59 rabbida φ x n Z dom n Z x A B n | y n Z y B = x n Z dom n Z x A B n | y n Z y n Z x A B n x
61 36 60 eqtrd φ x n Z A | y n Z y B = x n Z dom n Z x A B n | y n Z y n Z x A B n x
62 12 61 eqtrd φ D = x n Z dom n Z x A B n | y n Z y n Z x A B n x
63 2 62 alrimi φ x D = x n Z dom n Z x A B n | y n Z y n Z x A B n x
64 nfcv _ n
65 nfra1 n n Z y B
66 64 65 nfrex n y n Z y B
67 nfii1 _ n n Z A
68 66 67 nfrabw _ n x n Z A | y n Z y B
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 y B
75 74 biimpi x D x x n Z A | y n Z y B
76 rabidim1 x x n Z A | y n Z y B 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 infeq1d φ 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 y n Z x A B n x 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 y n Z x A B n x 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 y n Z x A B n x 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 y n Z x A B n x 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 y n Z x A B n x = x n Z dom n Z x A B n | y n Z y n Z x A B n x
97 eqid x x n Z dom n Z x A B n | y n Z y n Z x A B n x 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 y n Z x A B n x sup ran n Z n Z x A B n x <
98 93 31 4 5 6 95 96 97 smfinf φ x x n Z dom n Z x A B n | y n Z y n Z x A B n x sup ran n Z n Z x A B n x < SMblFn S
99 92 98 eqeltrd φ G SMblFn S