Metamath Proof Explorer

Theorem smfsupmpt

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 smfsupmpt.n 
|- F/ n ph
smfsupmpt.x 
|- F/ x ph
smfsupmpt.y 
|- F/ y ph
smfsupmpt.m 
|- ( ph -> M e. ZZ )
smfsupmpt.z 
|- Z = ( ZZ>= ` M )
smfsupmpt.s 
|- ( ph -> S e. SAlg )
smfsupmpt.b 
|- ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )
smfsupmpt.f 
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfsupmpt.d 
|- D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y }
smfsupmpt.g 
|- G = ( x e. D |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )
Assertion smfsupmpt 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfsupmpt.n 
 |-  F/ n ph
2 smfsupmpt.x 
 |-  F/ x ph
3 smfsupmpt.y 
 |-  F/ y ph
4 smfsupmpt.m 
 |-  ( ph -> M e. ZZ )
5 smfsupmpt.z 
 |-  Z = ( ZZ>= ` M )
6 smfsupmpt.s 
 |-  ( ph -> S e. SAlg )
7 smfsupmpt.b 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B e. V )
8 smfsupmpt.f 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
9 smfsupmpt.d 
 |-  D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y }
10 smfsupmpt.g 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )
11 eqidd 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) = ( n e. Z |-> ( x e. A |-> B ) ) )
12 11 8 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = ( x e. A |-> B ) )
13 12 dmeqd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = dom ( x e. A |-> B ) )
14 nfcv 
 |-  F/_ x Z
15 14 nfcri 
 |-  F/ x n e. Z
16 2 15 nfan 
 |-  F/ x ( ph /\ n e. Z )
17 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
18 7 3expa 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V )
19 16 17 18 dmmptdf 
 |-  ( ( ph /\ n e. Z ) -> dom ( x e. A |-> B ) = A )
20 13 19 eqtr2d 
 |-  ( ( ph /\ n e. Z ) -> A = dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
21 1 20 iineq2d 
 |-  ( ph -> |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
22 nfcv 
 |-  F/_ x |^|_ n e. Z A
23 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
24 14 23 nfmpt 
 |-  F/_ x ( n e. Z |-> ( x e. A |-> B ) )
25 nfcv 
 |-  F/_ x n
26 24 25 nffv 
 |-  F/_ x ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
27 26 nfdm 
 |-  F/_ x dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
28 14 27 nfiin 
 |-  F/_ x |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
29 22 28 rabeqf 
 |-  ( |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z B <_ y } )
30 21 29 syl 
 |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z B <_ y } )
31 nfv 
 |-  F/ y x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
32 3 31 nfan 
 |-  F/ y ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
33 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
34 33 nfcri 
 |-  F/ n x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n )
35 1 34 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
36 simpll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ph )
37 simpr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> n e. Z )
38 eliinid 
 |-  ( ( x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
39 38 adantll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) )
40 13 19 eqtrd 
 |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A )
41 40 adantlr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A )
42 39 41 eleqtrd 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. A )
43 12 fveq1d 
 |-  ( ( ph /\ n e. Z ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
44 43 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) )
45 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> x e. A )
46 fvmpt4 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
47 45 7 46 syl2anc 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
48 44 47 eqtr2d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
49 48 breq1d 
 |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( B <_ y <-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y ) )
50 36 37 42 49 syl3anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ( B <_ y <-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y ) )
51 35 50 ralbida 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( A. n e. Z B <_ y <-> A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y ) )
52 32 51 rexbid 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( E. y e. RR A. n e. Z B <_ y <-> E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y ) )
53 2 52 rabbida 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z B <_ y } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } )
54 30 53 eqtrd 
 |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } )
55 9 54 syl5eq 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } )
56 nfcv 
 |-  F/_ n RR
57 nfra1 
 |-  F/ n A. n e. Z B <_ y
58 56 57 nfrex 
 |-  F/ n E. y e. RR A. n e. Z B <_ y
59 nfii1 
 |-  F/_ n |^|_ n e. Z A
60 58 59 nfrabw 
 |-  F/_ n { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y }
61 9 60 nfcxfr 
 |-  F/_ n D
62 61 nfcri 
 |-  F/ n x e. D
63 1 62 nfan 
 |-  F/ n ( ph /\ x e. D )
64 simpll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ph )
65 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> n e. Z )
66 rabidim1 
 |-  ( x e. { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z B <_ y } -> x e. |^|_ n e. Z A )
67 66 9 eleq2s 
 |-  ( x e. D -> x e. |^|_ n e. Z A )
68 eliinid 
 |-  ( ( x e. |^|_ n e. Z A /\ n e. Z ) -> x e. A )
69 67 68 sylan 
 |-  ( ( x e. D /\ n e. Z ) -> x e. A )
70 69 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. A )
71 64 65 70 48 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) )
72 63 71 mpteq2da 
 |-  ( ( ph /\ x e. D ) -> ( n e. Z |-> B ) = ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
73 72 rneqd 
 |-  ( ( ph /\ x e. D ) -> ran ( n e. Z |-> B ) = ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) )
74 73 supeq1d 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> B ) , RR , < ) = sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) )
75 2 55 74 mpteq12da 
 |-  ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
76 10 75 syl5eq 
 |-  ( ph -> G = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) )
77 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( x e. A |-> B ) )
78 1 8 fmptd2f 
 |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
79 eqid 
 |-  { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y }
80 eqid 
 |-  ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) )
81 77 24 4 5 6 78 79 80 smfsup 
 |-  ( ph -> ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) <_ y } |-> sup ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
82 76 81 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )