Metamath Proof Explorer

Theorem smfsuplem2

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 smfsuplem2.m 
|- ( ph -> M e. ZZ )
smfsuplem2.z 
|- Z = ( ZZ>= ` M )
smfsuplem2.s 
|- ( ph -> S e. SAlg )
smfsuplem2.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfsuplem2.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
smfsuplem2.g 
|- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
smfsuplem2.8 
|- ( ph -> A e. RR )
Assertion smfsuplem2 
|- ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfsuplem2.m 
 |-  ( ph -> M e. ZZ )
2 smfsuplem2.z 
 |-  Z = ( ZZ>= ` M )
3 smfsuplem2.s 
 |-  ( ph -> S e. SAlg )
4 smfsuplem2.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfsuplem2.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
6 smfsuplem2.g 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
7 smfsuplem2.8 
 |-  ( ph -> A e. RR )
8 nfcv 
 |-  F/_ n F
9 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
10 eqid 
 |-  ( SalGen ` ( topGen ` ran (,) ) ) = ( SalGen ` ( topGen ` ran (,) ) )
11 mnfxr 
 |-  -oo e. RR*
12 11 a1i 
 |-  ( ph -> -oo e. RR* )
13 12 7 9 10 iocborel 
 |-  ( ph -> ( -oo (,] A ) e. ( SalGen ` ( topGen ` ran (,) ) ) )
14 8 2 3 4 9 10 13 smfpimcc 
 |-  ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
15 1 adantr 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> M e. ZZ )
16 3 adantr 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> S e. SAlg )
17 4 adantr 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> F : Z --> ( SMblFn ` S ) )
18 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
19 18 dmeqd 
 |-  ( n = m -> dom ( F ` n ) = dom ( F ` m ) )
20 19 cbviinv 
 |-  |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m )
21 20 a1i 
 |-  ( x = w -> |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m ) )
22 fveq2 
 |-  ( x = w -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` w ) )
23 22 breq1d 
 |-  ( x = w -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` n ) ` w ) <_ y ) )
24 23 ralbidv 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. n e. Z ( ( F ` n ) ` w ) <_ y ) )
25 18 fveq1d 
 |-  ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) )
26 25 breq1d 
 |-  ( n = m -> ( ( ( F ` n ) ` w ) <_ y <-> ( ( F ` m ) ` w ) <_ y ) )
27 26 cbvralvw 
 |-  ( A. n e. Z ( ( F ` n ) ` w ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y )
28 27 a1i 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` w ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y ) )
29 24 28 bitrd 
 |-  ( x = w -> ( A. n e. Z ( ( F ` n ) ` x ) <_ y <-> A. m e. Z ( ( F ` m ) ` w ) <_ y ) )
30 29 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 ) )
31 21 30 cbvrabv2w 
 |-  { 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. y e. RR A. m e. Z ( ( F ` m ) ` w ) <_ y }
32 5 31 eqtri 
 |-  D = { w e. |^|_ m e. Z dom ( F ` m ) | E. y e. RR A. m e. Z ( ( F ` m ) ` w ) <_ y }
33 22 mpteq2dv 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` x ) ) = ( n e. Z |-> ( ( F ` n ) ` w ) ) )
34 25 cbvmptv 
 |-  ( n e. Z |-> ( ( F ` n ) ` w ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) )
35 34 a1i 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` w ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) ) )
36 33 35 eqtrd 
 |-  ( x = w -> ( n e. Z |-> ( ( F ` n ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) ) )
37 36 rneqd 
 |-  ( x = w -> ran ( n e. Z |-> ( ( F ` n ) ` x ) ) = ran ( m e. Z |-> ( ( F ` m ) ` w ) ) )
38 37 supeq1d 
 |-  ( x = w -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
39 38 cbvmptv 
 |-  ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( w e. D |-> sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
40 6 39 eqtri 
 |-  G = ( w e. D |-> sup ( ran ( m e. Z |-> ( ( F ` m ) ` w ) ) , RR , < ) )
41 7 adantr 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> A e. RR )
42 simprl 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> h : Z --> S )
43 simplrr 
 |-  ( ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) /\ m e. Z ) -> A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) )
44 18 cnveqd 
 |-  ( n = m -> `' ( F ` n ) = `' ( F ` m ) )
45 44 imaeq1d 
 |-  ( n = m -> ( `' ( F ` n ) " ( -oo (,] A ) ) = ( `' ( F ` m ) " ( -oo (,] A ) ) )
46 fveq2 
 |-  ( n = m -> ( h ` n ) = ( h ` m ) )
47 46 19 ineq12d 
 |-  ( n = m -> ( ( h ` n ) i^i dom ( F ` n ) ) = ( ( h ` m ) i^i dom ( F ` m ) ) )
48 45 47 eqeq12d 
 |-  ( n = m -> ( ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) <-> ( `' ( F ` m ) " ( -oo (,] A ) ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) )
49 48 rspccva 
 |-  ( ( A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) /\ m e. Z ) -> ( `' ( F ` m ) " ( -oo (,] A ) ) = ( ( h ` m ) i^i dom ( F ` m ) ) )
50 43 49 sylancom 
 |-  ( ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) /\ m e. Z ) -> ( `' ( F ` m ) " ( -oo (,] A ) ) = ( ( h ` m ) i^i dom ( F ` m ) ) )
51 15 2 16 17 32 40 41 42 50 smfsuplem1 
 |-  ( ( ph /\ ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) )
52 51 ex 
 |-  ( ph -> ( ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) ) )
53 52 exlimdv 
 |-  ( ph -> ( E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) ) )
54 14 53 mpd 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) )