Metamath Proof Explorer

Theorem smflimsuplem8

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 smflimsuplem8.m 
|- ( ph -> M e. ZZ )
smflimsuplem8.z 
|- Z = ( ZZ>= ` M )
smflimsuplem8.s 
|- ( ph -> S e. SAlg )
smflimsuplem8.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem8.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
smflimsuplem8.g 
|- G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
smflimsuplem8.e 
|- E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem8.h 
|- H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
Assertion smflimsuplem8 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem8.m 
 |-  ( ph -> M e. ZZ )
2 smflimsuplem8.z 
 |-  Z = ( ZZ>= ` M )
3 smflimsuplem8.s 
 |-  ( ph -> S e. SAlg )
4 smflimsuplem8.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smflimsuplem8.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
6 smflimsuplem8.g 
 |-  G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7 smflimsuplem8.e 
 |-  E = ( k e. Z |-> { x e. |^|_ m e. ( ZZ>= ` k ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
8 smflimsuplem8.h 
 |-  H = ( k e. Z |-> ( x e. ( E ` k ) |-> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
9 6 a1i 
 |-  ( ph -> G = ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) )
10 1 2 3 4 5 7 8 smflimsuplem7 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } )
11 rabidim1 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
12 eliun 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
13 11 12 sylib 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
14 13 5 eleq2s 
 |-  ( x e. D -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
15 14 adantl 
 |-  ( ( ph /\ x e. D ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
16 nfv 
 |-  F/ n ( ph /\ x e. D )
17 nfv 
 |-  F/ n ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) )
18 nfv 
 |-  F/ k ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
19 nfv 
 |-  F/ m ( ph /\ x e. D )
20 nfv 
 |-  F/ m n e. Z
21 nfcv 
 |-  F/_ m x
22 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
23 21 22 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
24 19 20 23 nf3an 
 |-  F/ m ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
25 1 adantr 
 |-  ( ( ph /\ x e. D ) -> M e. ZZ )
26 25 3ad2ant1 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> M e. ZZ )
27 3 adantr 
 |-  ( ( ph /\ x e. D ) -> S e. SAlg )
28 27 3ad2ant1 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> S e. SAlg )
29 4 adantr 
 |-  ( ( ph /\ x e. D ) -> F : Z --> ( SMblFn ` S ) )
30 29 3ad2ant1 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> F : Z --> ( SMblFn ` S ) )
31 rabidim2 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
32 31 5 eleq2s 
 |-  ( x e. D -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
33 fveq2 
 |-  ( m = y -> ( F ` m ) = ( F ` y ) )
34 33 fveq1d 
 |-  ( m = y -> ( ( F ` m ) ` x ) = ( ( F ` y ) ` x ) )
35 34 cbvmptv 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( y e. Z |-> ( ( F ` y ) ` x ) )
36 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
37 36 fveq1d 
 |-  ( z = y -> ( ( F ` z ) ` x ) = ( ( F ` y ) ` x ) )
38 37 cbvmptv 
 |-  ( z e. Z |-> ( ( F ` z ) ` x ) ) = ( y e. Z |-> ( ( F ` y ) ` x ) )
39 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
40 39 fveq1d 
 |-  ( z = w -> ( ( F ` z ) ` x ) = ( ( F ` w ) ` x ) )
41 40 cbvmptv 
 |-  ( z e. Z |-> ( ( F ` z ) ` x ) ) = ( w e. Z |-> ( ( F ` w ) ` x ) )
42 35 38 41 3eqtr2i 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( w e. Z |-> ( ( F ` w ) ` x ) )
43 42 fveq2i 
 |-  ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( w e. Z |-> ( ( F ` w ) ` x ) ) )
44 43 eleq1i 
 |-  ( ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR <-> ( limsup ` ( w e. Z |-> ( ( F ` w ) ` x ) ) ) e. RR )
45 32 44 sylib 
 |-  ( x e. D -> ( limsup ` ( w e. Z |-> ( ( F ` w ) ` x ) ) ) e. RR )
46 45 adantl 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( w e. Z |-> ( ( F ` w ) ` x ) ) ) e. RR )
47 46 3ad2ant1 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( limsup ` ( w e. Z |-> ( ( F ` w ) ` x ) ) ) e. RR )
48 47 44 sylibr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
49 simp2 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> n e. Z )
50 simp3 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
51 18 24 26 2 28 30 7 8 48 49 50 smflimsuplem5 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( k e. ( ZZ>= ` n ) |-> ( ( H ` k ) ` x ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) )
52 fvexd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) e. _V )
53 2 fvexi 
 |-  Z e. _V
54 53 a1i 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> Z e. _V )
55 2 49 eluzelz2d 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> n e. ZZ )
56 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
57 55 uzidd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> n e. ( ZZ>= ` n ) )
58 57 uzssd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` n ) )
59 2 49 uzssd2 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) C_ Z )
60 fvexd 
 |-  ( ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( H ` k ) ` x ) e. _V )
61 18 52 54 55 56 58 59 60 climeqmpt 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ( k e. ( ZZ>= ` n ) |-> ( ( H ` k ) ` x ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) <-> ( k e. Z |-> ( ( H ` k ) ` x ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) ) )
62 51 61 mpbid 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) )
63 simp1l 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ph )
64 nfv 
 |-  F/ m ph
65 64 20 nfan 
 |-  F/ m ( ph /\ n e. Z )
66 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
67 66 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ZZ )
68 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> M e. ZZ )
69 fvexd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` x ) e. _V )
70 fvexd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. Z ) -> ( ( F ` m ) ` x ) e. _V )
71 65 67 68 56 2 69 70 limsupequzmpt 
 |-  ( ( ph /\ n e. Z ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
72 63 49 71 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
73 62 72 breqtrd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( k e. Z |-> ( ( H ` k ) ` x ) ) ~~> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
74 73 climfvd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) )
75 74 3exp 
 |-  ( ( ph /\ x e. D ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) ) ) )
76 16 17 75 rexlimd 
 |-  ( ( ph /\ x e. D ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) ) )
77 15 76 mpd 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) )
78 10 77 mpteq12dva 
 |-  ( ph -> ( x e. D |-> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) ) )
79 9 78 eqtrd 
 |-  ( ph -> G = ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) ) )
80 1 2 3 4 7 8 smflimsuplem3 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ k e. ( ZZ>= ` n ) dom ( H ` k ) | ( k e. Z |-> ( ( H ` k ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( k e. Z |-> ( ( H ` k ) ` x ) ) ) ) e. ( SMblFn ` S ) )
81 79 80 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )