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 
|- ( ph -> M e. ZZ )
smfsuplem3.z 
|- Z = ( ZZ>= ` M )
smfsuplem3.s 
|- ( ph -> S e. SAlg )
smfsuplem3.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfsuplem3.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
smfsuplem3.g 
|- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
Assertion smfsuplem3 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfsuplem3.m 
 |-  ( ph -> M e. ZZ )
2 smfsuplem3.z 
 |-  Z = ( ZZ>= ` M )
3 smfsuplem3.s 
 |-  ( ph -> S e. SAlg )
4 smfsuplem3.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfsuplem3.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
6 smfsuplem3.g 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
7 nfv 
 |-  F/ a ph
8 ssrab2 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } C_ |^|_ n e. Z dom ( F ` n )
9 5 8 eqsstri 
 |-  D C_ |^|_ n e. Z dom ( F ` n )
10 9 a1i 
 |-  ( ph -> D C_ |^|_ n e. Z dom ( F ` n ) )
11 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
12 1 11 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
13 12 2 eleqtrrdi 
 |-  ( ph -> M e. Z )
14 fveq2 
 |-  ( n = M -> ( F ` n ) = ( F ` M ) )
15 14 dmeqd 
 |-  ( n = M -> dom ( F ` n ) = dom ( F ` M ) )
16 4 13 ffvelrnd 
 |-  ( ph -> ( F ` M ) e. ( SMblFn ` S ) )
17 eqid 
 |-  dom ( F ` M ) = dom ( F ` M )
18 3 16 17 smfdmss 
 |-  ( ph -> dom ( F ` M ) C_ U. S )
19 13 15 18 iinssd 
 |-  ( ph -> |^|_ n e. Z dom ( F ` n ) C_ U. S )
20 10 19 sstrd 
 |-  ( ph -> D C_ U. S )
21 nfv 
 |-  F/ n ( ph /\ x e. D )
22 13 ne0d 
 |-  ( ph -> Z =/= (/) )
23 22 adantr 
 |-  ( ( ph /\ x e. D ) -> Z =/= (/) )
24 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
25 4 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
26 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
27 24 25 26 smff 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
28 27 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
29 iinss2 
 |-  ( n e. Z -> |^|_ n e. Z dom ( F ` n ) C_ dom ( F ` n ) )
30 29 adantl 
 |-  ( ( x e. D /\ n e. Z ) -> |^|_ n e. Z dom ( F ` n ) C_ dom ( F ` n ) )
31 9 sseli 
 |-  ( x e. D -> x e. |^|_ n e. Z dom ( F ` n ) )
32 31 adantr 
 |-  ( ( x e. D /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) )
33 30 32 sseldd 
 |-  ( ( x e. D /\ n e. Z ) -> x e. dom ( F ` n ) )
34 33 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. dom ( F ` n ) )
35 28 34 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
36 5 rabeq2i 
 |-  ( x e. D <-> ( x e. |^|_ n e. Z dom ( F ` n ) /\ E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) )
37 36 simprbi 
 |-  ( x e. D -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
38 37 adantl 
 |-  ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
39 21 23 35 38 suprclrnmpt 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
40 39 6 fmptd 
 |-  ( ph -> G : D --> RR )
41 1 adantr 
 |-  ( ( ph /\ a e. RR ) -> M e. ZZ )
42 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
43 4 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : Z --> ( SMblFn ` S ) )
44 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
45 41 2 42 43 5 6 44 smfsuplem2 
 |-  ( ( ph /\ a e. RR ) -> ( `' G " ( -oo (,] a ) ) e. ( S |`t D ) )
46 7 3 20 40 45 issmfle2d 
 |-  ( ph -> G e. ( SMblFn ` S ) )