Metamath Proof Explorer

Theorem smfliminf

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses smfliminf.n 
|- F/_ m F
smfliminf.x 
|- F/_ x F
smfliminf.m 
|- ( ph -> M e. ZZ )
smfliminf.z 
|- Z = ( ZZ>= ` M )
smfliminf.s 
|- ( ph -> S e. SAlg )
smfliminf.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfliminf.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
smfliminf.g 
|- G = ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
Assertion smfliminf 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfliminf.n 
 |-  F/_ m F
2 smfliminf.x 
 |-  F/_ x F
3 smfliminf.m 
 |-  ( ph -> M e. ZZ )
4 smfliminf.z 
 |-  Z = ( ZZ>= ` M )
5 smfliminf.s 
 |-  ( ph -> S e. SAlg )
6 smfliminf.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smfliminf.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
8 smfliminf.g 
 |-  G = ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
9 nfcv 
 |-  F/_ i |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
10 nfcv 
 |-  F/_ n |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
11 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
12 11 iineq1d 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
13 nfcv 
 |-  F/_ k ( F ` m )
14 13 nfdm 
 |-  F/_ k dom ( F ` m )
15 nfcv 
 |-  F/_ m k
16 1 15 nffv 
 |-  F/_ m ( F ` k )
17 16 nfdm 
 |-  F/_ m dom ( F ` k )
18 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
19 18 dmeqd 
 |-  ( m = k -> dom ( F ` m ) = dom ( F ` k ) )
20 14 17 19 cbviin 
 |-  |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) = |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
21 20 a1i 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) = |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) )
22 12 21 eqtrd 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) )
23 9 10 22 cbviun 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
24 23 rabeqi 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } = { x e. U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
25 nfcv 
 |-  F/_ x Z
26 nfcv 
 |-  F/_ x ( ZZ>= ` i )
27 nfcv 
 |-  F/_ x k
28 2 27 nffv 
 |-  F/_ x ( F ` k )
29 28 nfdm 
 |-  F/_ x dom ( F ` k )
30 26 29 nfiin 
 |-  F/_ x |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
31 25 30 nfiun 
 |-  F/_ x U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
32 nfcv 
 |-  F/_ y U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k )
33 nfv 
 |-  F/ y ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR
34 nfcv 
 |-  F/_ x liminf
35 nfcv 
 |-  F/_ x y
36 28 35 nffv 
 |-  F/_ x ( ( F ` k ) ` y )
37 25 36 nfmpt 
 |-  F/_ x ( k e. Z |-> ( ( F ` k ) ` y ) )
38 34 37 nffv 
 |-  F/_ x ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) )
39 nfcv 
 |-  F/_ x RR
40 38 39 nfel 
 |-  F/ x ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) e. RR
41 nfv 
 |-  F/ m x = y
42 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
43 42 adantr 
 |-  ( ( x = y /\ m e. Z ) -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
44 41 43 mpteq2da 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` y ) ) )
45 nfcv 
 |-  F/_ k ( ( F ` m ) ` y )
46 nfcv 
 |-  F/_ m y
47 16 46 nffv 
 |-  F/_ m ( ( F ` k ) ` y )
48 18 fveq1d 
 |-  ( m = k -> ( ( F ` m ) ` y ) = ( ( F ` k ) ` y ) )
49 45 47 48 cbvmpt 
 |-  ( m e. Z |-> ( ( F ` m ) ` y ) ) = ( k e. Z |-> ( ( F ` k ) ` y ) )
50 49 a1i 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` y ) ) = ( k e. Z |-> ( ( F ` k ) ` y ) ) )
51 44 50 eqtrd 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( k e. Z |-> ( ( F ` k ) ` y ) ) )
52 51 fveq2d 
 |-  ( x = y -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) )
53 52 eleq1d 
 |-  ( x = y -> ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR <-> ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) e. RR ) )
54 31 32 33 40 53 cbvrabw 
 |-  { x e. U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } = { y e. U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) | ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) e. RR }
55 7 24 54 3eqtri 
 |-  D = { y e. U_ i e. Z |^|_ k e. ( ZZ>= ` i ) dom ( F ` k ) | ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) e. RR }
56 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
57 7 56 nfcxfr 
 |-  F/_ x D
58 nfcv 
 |-  F/_ y D
59 nfcv 
 |-  F/_ y ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
60 57 58 59 38 52 cbvmptf 
 |-  ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( y e. D |-> ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) )
61 8 60 eqtri 
 |-  G = ( y e. D |-> ( liminf ` ( k e. Z |-> ( ( F ` k ) ` y ) ) ) )
62 3 4 5 6 55 61 smfliminflem 
 |-  ( ph -> G e. ( SMblFn ` S ) )