Metamath Proof Explorer

Theorem smflimsuplem6

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem6.a 
|- F/ n ph
smflimsuplem6.b 
|- F/ m ph
smflimsuplem6.m 
|- ( ph -> M e. ZZ )
smflimsuplem6.z 
|- Z = ( ZZ>= ` M )
smflimsuplem6.s 
|- ( ph -> S e. SAlg )
smflimsuplem6.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem6.e 
|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem6.h 
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
smflimsuplem6.r 
|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
smflimsuplem6.n 
|- ( ph -> N e. Z )
smflimsuplem6.x 
|- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
Assertion smflimsuplem6 
|- ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 smflimsuplem6.a 
 |-  F/ n ph
2 smflimsuplem6.b 
 |-  F/ m ph
3 smflimsuplem6.m 
 |-  ( ph -> M e. ZZ )
4 smflimsuplem6.z 
 |-  Z = ( ZZ>= ` M )
5 smflimsuplem6.s 
 |-  ( ph -> S e. SAlg )
6 smflimsuplem6.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smflimsuplem6.e 
 |-  E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
8 smflimsuplem6.h 
 |-  H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
9 smflimsuplem6.r 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
10 smflimsuplem6.n 
 |-  ( ph -> N e. Z )
11 smflimsuplem6.x 
 |-  ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
12 4 fvexi 
 |-  Z e. _V
13 12 a1i 
 |-  ( ph -> Z e. _V )
14 13 mptexd 
 |-  ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. _V )
15 fvexd 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) e. _V )
16 1 2 3 4 5 6 7 8 9 10 11 smflimsuplem5 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )
17 fvexd 
 |-  ( ph -> ( ZZ>= ` N ) e. _V )
18 4 eluzelz2 
 |-  ( N e. Z -> N e. ZZ )
19 10 18 syl 
 |-  ( ph -> N e. ZZ )
20 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
21 4 eleq2i 
 |-  ( N e. Z <-> N e. ( ZZ>= ` M ) )
22 21 biimpi 
 |-  ( N e. Z -> N e. ( ZZ>= ` M ) )
23 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
24 22 23 syl 
 |-  ( N e. Z -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
25 24 4 sseqtrrdi 
 |-  ( N e. Z -> ( ZZ>= ` N ) C_ Z )
26 10 25 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ Z )
27 ssid 
 |-  ( ZZ>= ` N ) C_ ( ZZ>= ` N )
28 27 a1i 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` N ) )
29 fvexd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` X ) e. _V )
30 1 13 17 19 20 26 28 29 climeqmpt 
 |-  ( ph -> ( ( n e. Z |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) <-> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) ) )
31 16 30 mpbird 
 |-  ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )
32 breldmg 
 |-  ( ( ( n e. Z |-> ( ( H ` n ) ` X ) ) e. _V /\ ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) e. _V /\ ( n e. Z |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) ) -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. dom ~~> )
33 14 15 31 32 syl3anc 
 |-  ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. dom ~~> )