Metamath Proof Explorer

Theorem smfsup

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

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

Proof

Step Hyp Ref Expression
1 smfsup.n 
 |-  F/_ n F
2 smfsup.x 
 |-  F/_ x F
3 smfsup.m 
 |-  ( ph -> M e. ZZ )
4 smfsup.z 
 |-  Z = ( ZZ>= ` M )
5 smfsup.s 
 |-  ( ph -> S e. SAlg )
6 smfsup.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smfsup.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
8 smfsup.g 
 |-  G = ( x e. D |-> sup ( 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 ( ( F ` n ) ` x ) <_ y
16 nfcv 
 |-  F/_ x RR
17 nfcv 
 |-  F/_ x w
18 12 17 nffv 
 |-  F/_ x ( ( F ` m ) ` w )
19 nfcv 
 |-  F/_ x <_
20 nfcv 
 |-  F/_ x z
21 18 19 20 nfbr 
 |-  F/ x ( ( F ` m ) ` w ) <_ z
22 10 21 nfralw 
 |-  F/ x A. m e. Z ( ( F ` m ) ` w ) <_ z
23 16 22 nfrex 
 |-  F/ x E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z
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 breq1d 
 |-  ( x = w -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` n ) ` w ) <_ y ) )
34 33 ralbidv 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. n e. Z ( ( F ` n ) ` w ) <_ y ) )
35 nfv 
 |-  F/ m ( ( F ` n ) ` w ) <_ y
36 nfcv 
 |-  F/_ n w
37 26 36 nffv 
 |-  F/_ n ( ( F ` m ) ` w )
38 nfcv 
 |-  F/_ n <_
39 nfcv 
 |-  F/_ n y
40 37 38 39 nfbr 
 |-  F/ n ( ( F ` m ) ` w ) <_ y
41 28 fveq1d 
 |-  ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) )
42 41 breq1d 
 |-  ( n = m -> ( ( ( F ` n ) ` w ) <_ y <-> ( ( F ` m ) ` w ) <_ y ) )
43 35 40 42 cbvralw 
 |-  ( A. n e. Z ( ( F ` n ) ` w ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y )
44 43 a1i 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` w ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y ) )
45 34 44 bitrd 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y ) )
46 45 rexbidv 
 |-  ( x = w -> ( E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y <-> E. y e. RR A. m e. Z ( ( F ` m ) ` w ) <_ y ) )
47 breq2 
 |-  ( y = z -> ( ( ( F ` m ) ` w ) <_ y <-> ( ( F ` m ) ` w ) <_ z ) )
48 47 ralbidv 
 |-  ( y = z -> ( A. m e. Z ( ( F ` m ) ` w ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ z ) )
49 48 cbvrexvw 
 |-  ( E. y e. RR A. m e. Z ( ( F ` m ) ` w ) <_ y <-> E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z )
50 49 a1i 
 |-  ( x = w -> ( E. y e. RR A. m e. Z ( ( F ` m ) ` w ) <_ y <-> E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z ) )
51 46 50 bitrd 
 |-  ( x = w -> ( E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y <-> E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z ) )
52 9 14 15 23 31 51 cbvrabcsfw 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z }
53 7 52 eqtri 
 |-  D = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z ( ( F ` m ) ` w ) <_ z }
54 nfrab1 
 |-  F/_ x { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
55 7 54 nfcxfr 
 |-  F/_ x D
56 nfcv 
 |-  F/_ w D
57 nfcv 
 |-  F/_ w sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < )
58 10 18 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 nfsup 
 |-  F/_ x sup ( 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 37 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 supeq1d 
 |-  ( x = w -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
69 55 56 57 61 68 cbvmptf 
 |-  ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( w e. D |-> sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
70 8 69 eqtri 
 |-  G = ( w e. D |-> sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
71 3 4 5 6 53 70 smfsuplem3 
 |-  ( ph -> G e. ( SMblFn ` S ) )