Metamath Proof Explorer

Theorem smfinf

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfinf.n 
|- F/_ n F
smfinf.x 
|- F/_ x F
smfinf.m 
|- ( ph -> M e. ZZ )
smfinf.z 
|- Z = ( ZZ>= ` M )
smfinf.s 
|- ( ph -> S e. SAlg )
smfinf.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfinf.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
smfinf.g 
|- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
Assertion smfinf 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfinf.n 
 |-  F/_ n F
2 smfinf.x 
 |-  F/_ x F
3 smfinf.m 
 |-  ( ph -> M e. ZZ )
4 smfinf.z 
 |-  Z = ( ZZ>= ` M )
5 smfinf.s 
 |-  ( ph -> S e. SAlg )
6 smfinf.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smfinf.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
8 smfinf.g 
 |-  G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
9 nfcv 
 |-  F/_ w |^|_ n e. Z dom ( F ` n )
10 nfcv 
 |-  F/_ x Z
11 nfcv 
 |-  F/_ x m
12 2 11 nffv 
 |-  F/_ x ( F ` m )
13 12 nfdm 
 |-  F/_ x dom ( F ` m )
14 10 13 nfiin 
 |-  F/_ x |^|_ m e. Z dom ( F ` m )
15 nfv 
 |-  F/ w E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x )
16 nfcv 
 |-  F/_ x RR
17 nfcv 
 |-  F/_ x z
18 nfcv 
 |-  F/_ x <_
19 nfcv 
 |-  F/_ x w
20 12 19 nffv 
 |-  F/_ x ( ( F ` m ) ` w )
21 17 18 20 nfbr 
 |-  F/ x z <_ ( ( F ` m ) ` w )
22 10 21 nfralw 
 |-  F/ x A. m e. Z z <_ ( ( F ` m ) ` w )
23 16 22 nfrex 
 |-  F/ x E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w )
24 nfcv 
 |-  F/_ m dom ( F ` n )
25 nfcv 
 |-  F/_ n m
26 1 25 nffv 
 |-  F/_ n ( F ` m )
27 26 nfdm 
 |-  F/_ n dom ( F ` m )
28 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
29 28 dmeqd 
 |-  ( n = m -> dom ( F ` n ) = dom ( F ` m ) )
30 24 27 29 cbviin 
 |-  |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m )
31 30 a1i 
 |-  ( x = w -> |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m ) )
32 fveq2 
 |-  ( x = w -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` w ) )
33 32 breq2d 
 |-  ( x = w -> ( y <_ ( ( F ` n ) ` x ) <-> y <_ ( ( F ` n ) ` w ) ) )
34 33 ralbidv 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. n e. Z y <_ ( ( F ` n ) ` w ) ) )
35 nfv 
 |-  F/ m y <_ ( ( F ` n ) ` w )
36 nfcv 
 |-  F/_ n y
37 nfcv 
 |-  F/_ n <_
38 nfcv 
 |-  F/_ n w
39 26 38 nffv 
 |-  F/_ n ( ( F ` m ) ` w )
40 36 37 39 nfbr 
 |-  F/ n y <_ ( ( F ` m ) ` w )
41 28 fveq1d 
 |-  ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) )
42 41 breq2d 
 |-  ( n = m -> ( y <_ ( ( F ` n ) ` w ) <-> y <_ ( ( F ` m ) ` w ) ) )
43 35 40 42 cbvralw 
 |-  ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) )
44 43 a1i 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
45 34 44 bitrd 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
46 45 rexbidv 
 |-  ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
47 breq1 
 |-  ( y = z -> ( y <_ ( ( F ` m ) ` w ) <-> z <_ ( ( F ` m ) ` w ) ) )
48 47 ralbidv 
 |-  ( y = z -> ( A. m e. Z y <_ ( ( F ` m ) ` w ) <-> A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
49 48 cbvrexvw 
 |-  ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) )
50 49 a1i 
 |-  ( x = w -> ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
51 46 50 bitrd 
 |-  ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
52 9 14 15 23 31 51 cbvrabcsfw 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) }
53 7 52 eqtri 
 |-  D = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) }
54 nfrab1 
 |-  F/_ x { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
55 7 54 nfcxfr 
 |-  F/_ x D
56 nfcv 
 |-  F/_ w D
57 nfcv 
 |-  F/_ w inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < )
58 10 20 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` w ) )
59 58 nfrn 
 |-  F/_ x ran ( m e. Z |-> ( ( F ` m ) ` w ) )
60 nfcv 
 |-  F/_ x <
61 59 16 60 nfinf 
 |-  F/_ x inf ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < )
62 32 mpteq2dv 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` x ) ) = ( n e. Z |-> ( ( F ` n ) ` w ) ) )
63 nfcv 
 |-  F/_ m ( ( F ` n ) ` w )
64 63 39 41 cbvmpt 
 |-  ( n e. Z |-> ( ( F ` n ) ` w ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) )
65 64 a1i 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` w ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) ) )
66 62 65 eqtrd 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) ) )
67 66 rneqd 
 |-  ( x = w -> ran ( n e. Z |-> ( ( F ` n ) ` x ) ) = ran ( m e. Z |-> ( ( F ` m ) ` w ) ) )
68 67 infeq1d 
 |-  ( x = w -> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) = inf ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
69 55 56 57 61 68 cbvmptf 
 |-  ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( w e. D |-> inf ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
70 8 69 eqtri 
 |-  G = ( w e. D |-> inf ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
71 3 4 5 6 53 70 smfinflem 
 |-  ( ph -> G e. ( SMblFn ` S ) )