Metamath Proof Explorer

Theorem smfsupxr

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 smfsupxr.n 
|- F/_ n F
smfsupxr.x 
|- F/_ x F
smfsupxr.m 
|- ( ph -> M e. ZZ )
smfsupxr.z 
|- Z = ( ZZ>= ` M )
smfsupxr.s 
|- ( ph -> S e. SAlg )
smfsupxr.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfsupxr.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR }
smfsupxr.g 
|- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) )
Assertion smfsupxr 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfsupxr.n 
 |-  F/_ n F
2 smfsupxr.x 
 |-  F/_ x F
3 smfsupxr.m 
 |-  ( ph -> M e. ZZ )
4 smfsupxr.z 
 |-  Z = ( ZZ>= ` M )
5 smfsupxr.s 
 |-  ( ph -> S e. SAlg )
6 smfsupxr.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smfsupxr.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR }
8 smfsupxr.g 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) )
9 8 a1i 
 |-  ( ph -> G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) ) )
10 7 a1i 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR } )
11 nfv 
 |-  F/ n ph
12 nfcv 
 |-  F/_ n x
13 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( F ` n )
14 12 13 nfel 
 |-  F/ n x e. |^|_ n e. Z dom ( F ` n )
15 11 14 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) )
16 3 4 uzn0d 
 |-  ( ph -> Z =/= (/) )
17 16 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> Z =/= (/) )
18 5 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
19 6 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
20 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
21 18 19 20 smff 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
22 21 adantlr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
23 eliinid 
 |-  ( ( x e. |^|_ n e. Z dom ( F ` n ) /\ n e. Z ) -> x e. dom ( F ` n ) )
24 23 adantll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> x e. dom ( F ` n ) )
25 22 24 ffvelcdmd 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
26 15 17 25 supxrre3rnmpt 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR <-> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) )
27 26 rabbidva 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } )
28 10 27 eqtrd 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } )
29 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( ( F ` n ) ` x ) )
30 29 nfrn 
 |-  F/_ n ran ( n e. Z |-> ( ( F ` n ) ` x ) )
31 nfcv 
 |-  F/_ n RR*
32 nfcv 
 |-  F/_ n <
33 30 31 32 nfsup 
 |-  F/_ n sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < )
34 nfcv 
 |-  F/_ n RR
35 33 34 nfel 
 |-  F/ n sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR
36 35 13 nfrabw 
 |-  F/_ n { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR }
37 7 36 nfcxfr 
 |-  F/_ n D
38 12 37 nfel 
 |-  F/ n x e. D
39 11 38 nfan 
 |-  F/ n ( ph /\ x e. D )
40 16 adantr 
 |-  ( ( ph /\ x e. D ) -> Z =/= (/) )
41 21 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
42 nfcv 
 |-  F/_ x Z
43 nfcv 
 |-  F/_ x n
44 2 43 nffv 
 |-  F/_ x ( F ` n )
45 44 nfdm 
 |-  F/_ x dom ( F ` n )
46 42 45 nfiin 
 |-  F/_ x |^|_ n e. Z dom ( F ` n )
47 46 ssrab2f 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR } C_ |^|_ n e. Z dom ( F ` n )
48 7 47 eqsstri 
 |-  D C_ |^|_ n e. Z dom ( F ` n )
49 id 
 |-  ( x e. D -> x e. D )
50 48 49 sselid 
 |-  ( x e. D -> x e. |^|_ n e. Z dom ( F ` n ) )
51 50 23 sylan 
 |-  ( ( x e. D /\ n e. Z ) -> x e. dom ( F ` n ) )
52 51 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. dom ( F ` n ) )
53 41 52 ffvelcdmd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
54 49 7 eleqtrdi 
 |-  ( x e. D -> x e. { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR } )
55 rabidim2 
 |-  ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR } -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR )
56 54 55 syl 
 |-  ( x e. D -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR )
57 56 adantl 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR )
58 50 adantl 
 |-  ( ( ph /\ x e. D ) -> x e. |^|_ n e. Z dom ( F ` n ) )
59 58 26 syldan 
 |-  ( ( ph /\ x e. D ) -> ( sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) e. RR <-> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) )
60 57 59 mpbid 
 |-  ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
61 39 40 53 60 supxrrernmpt 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) = sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
62 28 61 mpteq12dva 
 |-  ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR* , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) )
63 9 62 eqtrd 
 |-  ( ph -> G = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) )
64 eqid 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
65 eqid 
 |-  ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
66 1 2 3 4 5 6 64 65 smfsup 
 |-  ( ph -> ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
67 63 66 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )