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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( 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 sseldi
 |-  ( 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 ffvelrnd
 |-  ( ( ( 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 ) )