Metamath Proof Explorer

Theorem smflimsuplem3

Description: The limit of the ( Hn ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 smflimsuplem3.m 
 |-  ( ph -> M e. ZZ )
2 smflimsuplem3.z 
 |-  Z = ( ZZ>= ` M )
3 smflimsuplem3.s 
 |-  ( ph -> S e. SAlg )
4 smflimsuplem3.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smflimsuplem3.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 } )
6 smflimsuplem3.h 
 |-  H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
7 nfv 
 |-  F/ n ph
8 nfv 
 |-  F/ x ph
9 nfv 
 |-  F/ k ph
10 fvex 
 |-  ( H ` n ) e. _V
11 10 dmex 
 |-  dom ( H ` n ) e. _V
12 11 a1i 
 |-  ( ( ph /\ n e. Z ) -> dom ( H ` n ) e. _V )
13 fvexd 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( H ` n ) ) -> ( ( H ` n ) ` x ) e. _V )
14 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
15 5 a1i 
 |-  ( ph -> 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 } ) )
16 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 }
17 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
18 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
19 17 18 uzn0d 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
20 fvex 
 |-  ( F ` m ) e. _V
21 20 dmex 
 |-  dom ( F ` m ) e. _V
22 21 rgenw 
 |-  A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
23 22 a1i 
 |-  ( n e. Z -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
24 19 23 iinexd 
 |-  ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
25 24 adantl 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
26 16 25 rabexd 
 |-  ( ( ph /\ 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 )
27 15 26 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
28 fvres 
 |-  ( m e. ( ZZ>= ` n ) -> ( ( F |` ( ZZ>= ` n ) ) ` m ) = ( F ` m ) )
29 28 eqcomd 
 |-  ( m e. ( ZZ>= ` n ) -> ( F ` m ) = ( ( F |` ( ZZ>= ` n ) ) ` m ) )
30 29 adantl 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) = ( ( F |` ( ZZ>= ` n ) ) ` m ) )
31 30 dmeqd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> dom ( F ` m ) = dom ( ( F |` ( ZZ>= ` n ) ) ` m ) )
32 31 iineq2dv 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) )
33 32 eleq2d 
 |-  ( ( ph /\ n e. Z ) -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) ) )
34 29 fveq1d 
 |-  ( m e. ( ZZ>= ` n ) -> ( ( F ` m ) ` x ) = ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) )
35 34 mpteq2ia 
 |-  ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) )
36 35 rneqi 
 |-  ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) )
37 36 supeq1i 
 |-  sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < )
38 37 a1i 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) )
39 38 eleq1d 
 |-  ( ( ph /\ n e. Z ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR ) )
40 33 39 anbi12d 
 |-  ( ( ph /\ n e. Z ) -> ( ( 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 |` ( ZZ>= ` n ) ) ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR ) ) )
41 40 rabbidva2 
 |-  ( ( ph /\ n e. Z ) -> { 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 |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } )
42 27 41 eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } )
43 42 38 mpteq12dv 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) ) )
44 nfcv 
 |-  F/_ m ( F |` ( ZZ>= ` n ) )
45 nfcv 
 |-  F/_ x ( F |` ( ZZ>= ` n ) )
46 17 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ZZ )
47 4 adantr 
 |-  ( ( ph /\ n e. Z ) -> F : Z --> ( SMblFn ` S ) )
48 2 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
49 48 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` M ) )
50 uzss 
 |-  ( n e. ( ZZ>= ` M ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` M ) )
51 49 50 syl 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ ( ZZ>= ` M ) )
52 51 2 sseqtrrdi 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
53 52 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
54 47 53 fssresd 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ZZ>= ` n ) ) : ( ZZ>= ` n ) --> ( SMblFn ` S ) )
55 eqid 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR }
56 eqid 
 |-  ( x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) ) = ( x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) )
57 44 45 46 18 14 54 55 56 smfsupxr 
 |-  ( ( ph /\ n e. Z ) -> ( x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( ( F |` ( ZZ>= ` n ) ) ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) e. RR } |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( ( F |` ( ZZ>= ` n ) ) ` m ) ` x ) ) , RR* , < ) ) e. ( SMblFn ` S ) )
58 43 57 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. ( SMblFn ` S ) )
59 58 6 fmptd 
 |-  ( ph -> H : Z --> ( SMblFn ` S ) )
60 59 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) e. ( SMblFn ` S ) )
61 eqid 
 |-  dom ( H ` n ) = dom ( H ` n )
62 14 60 61 smff 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) : dom ( H ` n ) --> RR )
63 62 feqmptd 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( x e. dom ( H ` n ) |-> ( ( H ` n ) ` x ) ) )
64 63 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. dom ( H ` n ) |-> ( ( H ` n ) ` x ) ) = ( H ` n ) )
65 64 60 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. dom ( H ` n ) |-> ( ( H ` n ) ` x ) ) e. ( SMblFn ` S ) )
66 eqid 
 |-  { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> } = { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> }
67 eqid 
 |-  ( x e. { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( n e. Z |-> ( ( H ` n ) ` x ) ) ) ) = ( x e. { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( n e. Z |-> ( ( H ` n ) ` x ) ) ) )
68 7 8 9 1 2 12 13 3 65 66 67 smflimmpt 
 |-  ( ph -> ( x e. { x e. U_ k e. Z |^|_ n e. ( ZZ>= ` k ) dom ( H ` n ) | ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( n e. Z |-> ( ( H ` n ) ` x ) ) ) ) e. ( SMblFn ` S ) )