Metamath Proof Explorer

Theorem smflimlem6

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem6.1 
|- ( ph -> M e. ZZ )
smflimlem6.2 
|- Z = ( ZZ>= ` M )
smflimlem6.3 
|- ( ph -> S e. SAlg )
smflimlem6.4 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimlem6.5 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
smflimlem6.6 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
smflimlem6.7 
|- ( ph -> A e. RR )
smflimlem6.8 
|- P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
Assertion smflimlem6 
|- ( ph -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smflimlem6.1 
 |-  ( ph -> M e. ZZ )
2 smflimlem6.2 
 |-  Z = ( ZZ>= ` M )
3 smflimlem6.3 
 |-  ( ph -> S e. SAlg )
4 smflimlem6.4 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smflimlem6.5 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
6 smflimlem6.6 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7 smflimlem6.7 
 |-  ( ph -> A e. RR )
8 smflimlem6.8 
 |-  P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
9 2 fvexi 
 |-  Z e. _V
10 nnex 
 |-  NN e. _V
11 9 10 xpex 
 |-  ( Z X. NN ) e. _V
12 11 a1i 
 |-  ( ph -> ( Z X. NN ) e. _V )
13 eqid 
 |-  { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) }
14 13 3 rabexd 
 |-  ( ph -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
15 14 adantr 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
16 15 ralrimivva 
 |-  ( ph -> A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
17 8 fnmpo 
 |-  ( A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V -> P Fn ( Z X. NN ) )
18 16 17 syl 
 |-  ( ph -> P Fn ( Z X. NN ) )
19 fnrndomg 
 |-  ( ( Z X. NN ) e. _V -> ( P Fn ( Z X. NN ) -> ran P ~<_ ( Z X. NN ) ) )
20 12 18 19 sylc 
 |-  ( ph -> ran P ~<_ ( Z X. NN ) )
21 2 uzct 
 |-  Z ~<_ _om
22 nnct 
 |-  NN ~<_ _om
23 21 22 pm3.2i 
 |-  ( Z ~<_ _om /\ NN ~<_ _om )
24 xpct 
 |-  ( ( Z ~<_ _om /\ NN ~<_ _om ) -> ( Z X. NN ) ~<_ _om )
25 23 24 ax-mp 
 |-  ( Z X. NN ) ~<_ _om
26 25 a1i 
 |-  ( ph -> ( Z X. NN ) ~<_ _om )
27 domtr 
 |-  ( ( ran P ~<_ ( Z X. NN ) /\ ( Z X. NN ) ~<_ _om ) -> ran P ~<_ _om )
28 20 26 27 syl2anc 
 |-  ( ph -> ran P ~<_ _om )
29 vex 
 |-  y e. _V
30 8 elrnmpog 
 |-  ( y e. _V -> ( y e. ran P <-> E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) )
31 29 30 ax-mp 
 |-  ( y e. ran P <-> E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
32 31 biimpi 
 |-  ( y e. ran P -> E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
33 32 adantl 
 |-  ( ( ph /\ y e. ran P ) -> E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
34 simp3 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) /\ y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) -> y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
35 3 adantr 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> S e. SAlg )
36 4 ffvelcdmda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
37 36 adantrr 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> ( F ` m ) e. ( SMblFn ` S ) )
38 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
39 7 adantr 
 |-  ( ( ph /\ k e. NN ) -> A e. RR )
40 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
41 40 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR )
42 39 41 readdcld 
 |-  ( ( ph /\ k e. NN ) -> ( A + ( 1 / k ) ) e. RR )
43 42 adantrl 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> ( A + ( 1 / k ) ) e. RR )
44 35 37 38 43 smfpreimalt 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } e. ( S |`t dom ( F ` m ) ) )
45 fvex 
 |-  ( F ` m ) e. _V
46 45 dmex 
 |-  dom ( F ` m ) e. _V
47 46 a1i 
 |-  ( ph -> dom ( F ` m ) e. _V )
48 elrest 
 |-  ( ( S e. SAlg /\ dom ( F ` m ) e. _V ) -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } e. ( S |`t dom ( F ` m ) ) <-> E. s e. S { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) ) )
49 3 47 48 syl2anc 
 |-  ( ph -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } e. ( S |`t dom ( F ` m ) ) <-> E. s e. S { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) ) )
50 49 adantr 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } e. ( S |`t dom ( F ` m ) ) <-> E. s e. S { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) ) )
51 44 50 mpbid 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> E. s e. S { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) )
52 rabn0 
 |-  ( { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } =/= (/) <-> E. s e. S { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) )
53 51 52 sylibr 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } =/= (/) )
54 53 3adant3 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) /\ y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } =/= (/) )
55 34 54 eqnetrd 
 |-  ( ( ph /\ ( m e. Z /\ k e. NN ) /\ y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) -> y =/= (/) )
56 55 3exp 
 |-  ( ph -> ( ( m e. Z /\ k e. NN ) -> ( y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) ) )
57 56 rexlimdvv 
 |-  ( ph -> ( E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) )
58 57 adantr 
 |-  ( ( ph /\ y e. ran P ) -> ( E. m e. Z E. k e. NN y = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) )
59 33 58 mpd 
 |-  ( ( ph /\ y e. ran P ) -> y =/= (/) )
60 28 59 axccd2 
 |-  ( ph -> E. c A. y e. ran P ( c ` y ) e. y )
61 1 adantr 
 |-  ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) -> M e. ZZ )
62 3 adantr 
 |-  ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) -> S e. SAlg )
63 4 adantr 
 |-  ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) -> F : Z --> ( SMblFn ` S ) )
64 7 adantr 
 |-  ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) -> A e. RR )
65 fvoveq1 
 |-  ( l = m -> ( c ` ( l P j ) ) = ( c ` ( m P j ) ) )
66 oveq2 
 |-  ( j = k -> ( m P j ) = ( m P k ) )
67 66 fveq2d 
 |-  ( j = k -> ( c ` ( m P j ) ) = ( c ` ( m P k ) ) )
68 65 67 cbvmpov 
 |-  ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) = ( m e. Z , k e. NN |-> ( c ` ( m P k ) ) )
69 nfcv 
 |-  F/_ k U_ n e. Z |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j )
70 nfcv 
 |-  F/_ j Z
71 nfcv 
 |-  F/_ j ( ZZ>= ` n )
72 nfcv 
 |-  F/_ j m
73 nfmpo2 
 |-  F/_ j ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) )
74 nfcv 
 |-  F/_ j k
75 72 73 74 nfov 
 |-  F/_ j ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k )
76 71 75 nfiin 
 |-  F/_ j |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k )
77 70 76 nfiun 
 |-  F/_ j U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k )
78 oveq2 
 |-  ( j = k -> ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
79 78 adantr 
 |-  ( ( j = k /\ i e. ( ZZ>= ` n ) ) -> ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
80 79 iineq2dv 
 |-  ( j = k -> |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
81 oveq1 
 |-  ( i = m -> ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) = ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
82 81 cbviinv 
 |-  |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) = |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k )
83 82 a1i 
 |-  ( j = k -> |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) = |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
84 80 83 eqtrd 
 |-  ( j = k -> |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
85 84 adantr 
 |-  ( ( j = k /\ n e. Z ) -> |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
86 85 iuneq2dv 
 |-  ( j = k -> U_ n e. Z |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k ) )
87 69 77 86 cbviin 
 |-  |^|_ j e. NN U_ n e. Z |^|_ i e. ( ZZ>= ` n ) ( i ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) j ) = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m ( l e. Z , j e. NN |-> ( c ` ( l P j ) ) ) k )
88 fveq2 
 |-  ( y = r -> ( c ` y ) = ( c ` r ) )
89 id 
 |-  ( y = r -> y = r )
90 88 89 eleq12d 
 |-  ( y = r -> ( ( c ` y ) e. y <-> ( c ` r ) e. r ) )
91 90 rspccva 
 |-  ( ( A. y e. ran P ( c ` y ) e. y /\ r e. ran P ) -> ( c ` r ) e. r )
92 91 adantll 
 |-  ( ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) /\ r e. ran P ) -> ( c ` r ) e. r )
93 61 2 62 63 5 6 64 8 68 87 92 smflimlem5 
 |-  ( ( ph /\ A. y e. ran P ( c ` y ) e. y ) -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) )
94 93 ex 
 |-  ( ph -> ( A. y e. ran P ( c ` y ) e. y -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) ) )
95 94 exlimdv 
 |-  ( ph -> ( E. c A. y e. ran P ( c ` y ) e. y -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) ) )
96 60 95 mpd 
 |-  ( ph -> { x e. D | ( G ` x ) <_ A } e. ( S |`t D ) )