Metamath Proof Explorer

Theorem smflimsuplem2

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 smflimsuplem2.p 
|- F/ m ph
smflimsuplem2.m 
|- ( ph -> M e. ZZ )
smflimsuplem2.z 
|- Z = ( ZZ>= ` M )
smflimsuplem2.s 
|- ( ph -> S e. SAlg )
smflimsuplem2.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem2.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 } )
smflimsuplem2.h 
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
smflimsuplem2.n 
|- ( ph -> n e. Z )
smflimsuplem2.r 
|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
smflimsuplem2.x 
|- ( ph -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
Assertion smflimsuplem2 
|- ( ph -> X e. dom ( H ` n ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem2.p 
 |-  F/ m ph
2 smflimsuplem2.m 
 |-  ( ph -> M e. ZZ )
3 smflimsuplem2.z 
 |-  Z = ( ZZ>= ` M )
4 smflimsuplem2.s 
 |-  ( ph -> S e. SAlg )
5 smflimsuplem2.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
6 smflimsuplem2.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 } )
7 smflimsuplem2.h 
 |-  H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
8 smflimsuplem2.n 
 |-  ( ph -> n e. Z )
9 smflimsuplem2.r 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
10 smflimsuplem2.x 
 |-  ( ph -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
11 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
12 8 3 eleqtrdi 
 |-  ( ph -> n e. ( ZZ>= ` M ) )
13 uzss 
 |-  ( n e. ( ZZ>= ` M ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` M ) )
14 12 13 syl 
 |-  ( ph -> ( ZZ>= ` n ) C_ ( ZZ>= ` M ) )
15 14 3 sseqtrrdi 
 |-  ( ph -> ( ZZ>= ` n ) C_ Z )
16 15 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ZZ>= ` n ) C_ Z )
17 simpr 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` n ) )
18 16 17 sseldd 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
19 4 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
20 5 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
21 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
22 19 20 21 smff 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
23 18 22 syldan 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
24 iinss2 
 |-  ( m e. ( ZZ>= ` n ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ dom ( F ` m ) )
25 24 adantl 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ dom ( F ` m ) )
26 10 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
27 25 26 sseldd 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> X e. dom ( F ` m ) )
28 23 27 ffvelrnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. RR )
29 nfmpt1 
 |-  F/_ m ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) )
30 nfmpt1 
 |-  F/_ m ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) )
31 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
32 12 31 syl 
 |-  ( ph -> n e. ZZ )
33 eqid 
 |-  ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) )
34 1 28 33 fmptdf 
 |-  ( ph -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) : ( ZZ>= ` n ) --> RR )
35 34 ffnd 
 |-  ( ph -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) Fn ( ZZ>= ` n ) )
36 nfcv 
 |-  F/_ m ( ZZ>= ` M )
37 fvexd 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( ( F ` m ) ` X ) e. _V )
38 36 1 37 mptfnd 
 |-  ( ph -> ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) Fn ( ZZ>= ` M ) )
39 33 a1i 
 |-  ( ph -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) )
40 fvexd 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. _V )
41 39 40 fvmpt2d 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` m ) = ( ( F ` m ) ` X ) )
42 18 3 eleqtrdi 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` M ) )
43 eqid 
 |-  ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) = ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) )
44 43 fvmpt2 
 |-  ( ( m e. ( ZZ>= ` M ) /\ ( ( F ` m ) ` X ) e. _V ) -> ( ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ` m ) = ( ( F ` m ) ` X ) )
45 42 40 44 syl2anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ` m ) = ( ( F ` m ) ` X ) )
46 41 45 eqtr4d 
 |-  ( ( ph /\ m e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` m ) = ( ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ` m ) )
47 1 29 30 32 35 2 38 32 46 limsupequz 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ) )
48 3 eqcomi 
 |-  ( ZZ>= ` M ) = Z
49 48 mpteq1i 
 |-  ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) )
50 49 fveq2i 
 |-  ( limsup ` ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) )
51 50 a1i 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` M ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
52 47 51 eqtrd 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
53 9 renepnfd 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) =/= +oo )
54 52 53 eqnetrd 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) =/= +oo )
55 1 11 28 54 limsupubuzmpt 
 |-  ( ph -> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y )
56 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
57 ne0i 
 |-  ( n e. ( ZZ>= ` n ) -> ( ZZ>= ` n ) =/= (/) )
58 32 56 57 3syl 
 |-  ( ph -> ( ZZ>= ` n ) =/= (/) )
59 1 58 28 supxrre3rnmpt 
 |-  ( ph -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR <-> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y ) )
60 55 59 mpbird 
 |-  ( ph -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR )
61 10 60 jca 
 |-  ( ph -> ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) )
62 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
63 62 mpteq2dv 
 |-  ( x = y -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
64 63 rneqd 
 |-  ( x = y -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
65 64 supeq1d 
 |-  ( x = y -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) )
66 65 eleq1d 
 |-  ( x = y -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR ) )
67 66 cbvrabv 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR }
68 67 eleq2i 
 |-  ( X e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } <-> X e. { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } )
69 fveq2 
 |-  ( y = X -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` X ) )
70 69 mpteq2dv 
 |-  ( y = X -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) )
71 70 rneqd 
 |-  ( y = X -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) )
72 71 supeq1d 
 |-  ( y = X -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) )
73 72 eleq1d 
 |-  ( y = X -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) )
74 73 elrab 
 |-  ( X e. { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } <-> ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) )
75 68 74 bitri 
 |-  ( X e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } <-> ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) )
76 61 75 sylibr 
 |-  ( ph -> X e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
77 id 
 |-  ( ph -> ph )
78 7 a1i 
 |-  ( ph -> H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ) )
79 nfcv 
 |-  F/_ x Z
80 nfrab1 
 |-  F/_ x { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
81 79 80 nfmpt 
 |-  F/_ x ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
82 6 81 nfcxfr 
 |-  F/_ x E
83 nfcv 
 |-  F/_ x n
84 82 83 nffv 
 |-  F/_ x ( E ` n )
85 fvex 
 |-  ( E ` n ) e. _V
86 84 85 mptexf 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V
87 86 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V )
88 78 87 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
89 77 8 88 syl2anc 
 |-  ( ph -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
90 89 dmeqd 
 |-  ( ph -> dom ( H ` n ) = dom ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
91 nfcv 
 |-  F/_ y ( E ` n )
92 nfcv 
 |-  F/_ y sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < )
93 nfcv 
 |-  F/_ x sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < )
94 84 91 92 93 65 cbvmptf 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( y e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) )
95 xrltso 
 |-  < Or RR*
96 95 supex 
 |-  sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. _V
97 96 a1i 
 |-  ( ( ph /\ y e. ( E ` n ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. _V )
98 94 97 dmmptd 
 |-  ( ph -> dom ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( E ` n ) )
99 eqid 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
100 fvex 
 |-  ( F ` m ) e. _V
101 100 dmex 
 |-  dom ( F ` m ) e. _V
102 101 rgenw 
 |-  A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
103 102 a1i 
 |-  ( ph -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
104 58 103 iinexd 
 |-  ( ph -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
105 99 104 rabexd 
 |-  ( ph -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V )
106 6 fvmpt2 
 |-  ( ( n e. Z /\ { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
107 8 105 106 syl2anc 
 |-  ( ph -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
108 90 98 107 3eqtrrd 
 |-  ( ph -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = dom ( H ` n ) )
109 76 108 eleqtrd 
 |-  ( ph -> X e. dom ( H ` n ) )