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 . The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Vincent Gonzalez, 30-Aug-2026)

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