Metamath Proof Explorer


Theorem smfsuplem3

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 smfsuplem3.m φ M
smfsuplem3.z Z = M
smfsuplem3.s φ S SAlg
smfsuplem3.f φ F : Z SMblFn S
smfsuplem3.d D = x n Z dom F n | y n Z F n x y
smfsuplem3.g G = x D sup ran n Z F n x <
Assertion smfsuplem3 φ G SMblFn S

Proof

Step Hyp Ref Expression
1 smfsuplem3.m φ M
2 smfsuplem3.z Z = M
3 smfsuplem3.s φ S SAlg
4 smfsuplem3.f φ F : Z SMblFn S
5 smfsuplem3.d D = x n Z dom F n | y n Z F n x y
6 smfsuplem3.g G = x D sup ran n Z F n x <
7 nfv a φ
8 ssrab2 x n Z dom F n | y n Z F n x y n Z dom F n
9 5 8 eqsstri D n Z dom F n
10 9 a1i φ D n Z dom F n
11 uzid M M M
12 1 11 syl φ M M
13 12 2 eleqtrrdi φ M Z
14 fveq2 n = M F n = F M
15 14 dmeqd n = M dom F n = dom F M
16 4 13 ffvelrnd φ F M SMblFn S
17 eqid dom F M = dom F M
18 3 16 17 smfdmss φ dom F M S
19 13 15 18 iinssd φ n Z dom F n S
20 10 19 sstrd φ D S
21 nfv n φ x D
22 13 ne0d φ Z
23 22 adantr φ x D Z
24 3 adantr φ n Z S SAlg
25 4 ffvelrnda φ n Z F n SMblFn S
26 eqid dom F n = dom F n
27 24 25 26 smff φ n Z F n : dom F n
28 27 adantlr φ x D n Z F n : dom F n
29 iinss2 n Z n Z dom F n dom F n
30 29 adantl x D n Z n Z dom F n dom F n
31 9 sseli x D x n Z dom F n
32 31 adantr x D n Z x n Z dom F n
33 30 32 sseldd x D n Z x dom F n
34 33 adantll φ x D n Z x dom F n
35 28 34 ffvelrnd φ x D n Z F n x
36 5 rabeq2i x D x n Z dom F n y n Z F n x y
37 36 simprbi x D y n Z F n x y
38 37 adantl φ x D y n Z F n x y
39 21 23 35 38 suprclrnmpt φ x D sup ran n Z F n x <
40 39 6 fmptd φ G : D
41 1 adantr φ a M
42 3 adantr φ a S SAlg
43 4 adantr φ a F : Z SMblFn S
44 simpr φ a a
45 41 2 42 43 5 6 44 smfsuplem2 φ a G -1 −∞ a S 𝑡 D
46 7 3 20 40 45 issmfle2d φ G SMblFn S