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 inf 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 inf 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 2 21 rabeqd φ x n Z A | y n Z y B = x n Z dom n Z x A B n | y n Z y B
23 nfv y x n Z dom n Z x A B n
24 3 23 nfan y φ x n Z dom n Z x A B n
25 nfii1 _ n n Z dom n Z x A B n
26 25 nfcri n x n Z dom n Z x A B n
27 1 26 nfan n φ x n Z dom n Z x A B n
28 simpll φ x n Z dom n Z x A B n n Z φ
29 simpr φ x n Z dom n Z x A B n n Z n Z
30 eliinid x n Z dom n Z x A B n n Z x dom n Z x A B n
31 30 adantll φ x n Z dom n Z x A B n n Z x dom n Z x A B n
32 13 19 eqtrd φ n Z dom n Z x A B n = A
33 32 adantlr φ x n Z dom n Z x A B n n Z dom n Z x A B n = A
34 31 33 eleqtrd φ x n Z dom n Z x A B n n Z x A
35 12 fveq1d φ n Z n Z x A B n x = x A B x
36 35 3adant3 φ n Z x A n Z x A B n x = x A B x
37 simp3 φ n Z x A x A
38 fvmpt4 x A B V x A B x = B
39 37 7 38 syl2anc φ n Z x A x A B x = B
40 36 39 eqtr2d φ n Z x A B = n Z x A B n x
41 40 breq2d φ n Z x A y B y n Z x A B n x
42 28 29 34 41 syl3anc φ x n Z dom n Z x A B n n Z y B y n Z x A B n x
43 27 42 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
44 24 43 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
45 2 44 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
46 22 45 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
47 9 46 eqtrid φ D = x n Z dom n Z x A B n | y n Z y n Z x A B n x
48 nfcv _ n
49 nfra1 n n Z y B
50 48 49 nfrexw n y n Z y B
51 nfii1 _ n n Z A
52 50 51 nfrabw _ n x n Z A | y n Z y B
53 9 52 nfcxfr _ n D
54 53 nfcri n x D
55 1 54 nfan n φ x D
56 simpll φ x D n Z φ
57 simpr φ x D n Z n Z
58 rabidim1 x x n Z A | y n Z y B x n Z A
59 58 9 eleq2s x D x n Z A
60 eliinid x n Z A n Z x A
61 59 60 sylan x D n Z x A
62 61 adantll φ x D n Z x A
63 56 57 62 40 syl3anc φ x D n Z B = n Z x A B n x
64 55 63 mpteq2da φ x D n Z B = n Z n Z x A B n x
65 64 rneqd φ x D ran n Z B = ran n Z n Z x A B n x
66 65 infeq1d φ x D inf ran n Z B < = inf ran n Z n Z x A B n x <
67 2 47 66 mpteq12da φ x D inf 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 inf ran n Z n Z x A B n x <
68 10 67 eqtrid φ G = x x n Z dom n Z x A B n | y n Z y n Z x A B n x inf ran n Z n Z x A B n x <
69 nfmpt1 _ n n Z x A B
70 nfmpt1 _ x x A B
71 14 70 nfmpt _ x n Z x A B
72 1 8 fmptd2f φ n Z x A B : Z SMblFn S
73 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
74 eqid x x n Z dom n Z x A B n | y n Z y n Z x A B n x inf 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 inf ran n Z n Z x A B n x <
75 69 71 4 5 6 72 73 74 smfinf φ x x n Z dom n Z x A B n | y n Z y n Z x A B n x inf ran n Z n Z x A B n x < SMblFn S
76 68 75 eqeltrd φ G SMblFn S