Metamath Proof Explorer

Theorem mbfinf

Description: The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses mbfinf.1 
|- Z = ( ZZ>= ` M )
mbfinf.2 
|- G = ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )
mbfinf.3 
|- ( ph -> M e. ZZ )
mbfinf.4 
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
mbfinf.5 
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
mbfinf.6 
|- ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z y <_ B )
Assertion mbfinf 
|- ( ph -> G e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfinf.1 
 |-  Z = ( ZZ>= ` M )
2 mbfinf.2 
 |-  G = ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )
3 mbfinf.3 
 |-  ( ph -> M e. ZZ )
4 mbfinf.4 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
5 mbfinf.5 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
6 mbfinf.6 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z y <_ B )
7 5 anass1rs 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR )
8 7 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR )
9 8 frnd 
 |-  ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) C_ RR )
10 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
11 3 10 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
12 11 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
13 12 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. Z )
14 eqid 
 |-  ( n e. Z |-> B ) = ( n e. Z |-> B )
15 14 7 dmmptd 
 |-  ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) = Z )
16 13 15 eleqtrrd 
 |-  ( ( ph /\ x e. A ) -> M e. dom ( n e. Z |-> B ) )
17 16 ne0d 
 |-  ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) =/= (/) )
18 dm0rn0 
 |-  ( dom ( n e. Z |-> B ) = (/) <-> ran ( n e. Z |-> B ) = (/) )
19 18 necon3bii 
 |-  ( dom ( n e. Z |-> B ) =/= (/) <-> ran ( n e. Z |-> B ) =/= (/) )
20 17 19 sylib 
 |-  ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) =/= (/) )
21 8 ffnd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) Fn Z )
22 breq2 
 |-  ( z = ( ( n e. Z |-> B ) ` m ) -> ( y <_ z <-> y <_ ( ( n e. Z |-> B ) ` m ) ) )
23 22 ralrn 
 |-  ( ( n e. Z |-> B ) Fn Z -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) ) )
24 21 23 syl 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) ) )
25 nfcv 
 |-  F/_ n y
26 nfcv 
 |-  F/_ n <_
27 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> B ) ` m )
28 25 26 27 nfbr 
 |-  F/ n y <_ ( ( n e. Z |-> B ) ` m )
29 nfv 
 |-  F/ m y <_ ( ( n e. Z |-> B ) ` n )
30 fveq2 
 |-  ( m = n -> ( ( n e. Z |-> B ) ` m ) = ( ( n e. Z |-> B ) ` n ) )
31 30 breq2d 
 |-  ( m = n -> ( y <_ ( ( n e. Z |-> B ) ` m ) <-> y <_ ( ( n e. Z |-> B ) ` n ) ) )
32 28 29 31 cbvralw 
 |-  ( A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) <-> A. n e. Z y <_ ( ( n e. Z |-> B ) ` n ) )
33 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> n e. Z )
34 14 fvmpt2 
 |-  ( ( n e. Z /\ B e. RR ) -> ( ( n e. Z |-> B ) ` n ) = B )
35 33 7 34 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B )
36 35 breq2d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( y <_ ( ( n e. Z |-> B ) ` n ) <-> y <_ B ) )
37 36 ralbidva 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. Z y <_ ( ( n e. Z |-> B ) ` n ) <-> A. n e. Z y <_ B ) )
38 32 37 syl5bb 
 |-  ( ( ph /\ x e. A ) -> ( A. m e. Z y <_ ( ( n e. Z |-> B ) ` m ) <-> A. n e. Z y <_ B ) )
39 24 38 bitrd 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) y <_ z <-> A. n e. Z y <_ B ) )
40 39 rexbidv 
 |-  ( ( ph /\ x e. A ) -> ( E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z <-> E. y e. RR A. n e. Z y <_ B ) )
41 6 40 mpbird 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z )
42 infrenegsup 
 |-  ( ( ran ( n e. Z |-> B ) C_ RR /\ ran ( n e. Z |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. Z |-> B ) y <_ z ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) )
43 9 20 41 42 syl3anc 
 |-  ( ( ph /\ x e. A ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) )
44 rabid 
 |-  ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) )
45 7 recnd 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. CC )
46 45 adantlr 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> B e. CC )
47 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> r e. RR )
48 47 recnd 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> r e. CC )
49 negcon2 
 |-  ( ( B e. CC /\ r e. CC ) -> ( B = -u r <-> r = -u B ) )
50 46 48 49 syl2anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( B = -u r <-> r = -u B ) )
51 eqcom 
 |-  ( r = -u B <-> -u B = r )
52 50 51 bitrdi 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( B = -u r <-> -u B = r ) )
53 35 adantlr 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B )
54 53 eqeq1d 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> B = -u r ) )
55 negex 
 |-  -u B e. _V
56 eqid 
 |-  ( n e. Z |-> -u B ) = ( n e. Z |-> -u B )
57 56 fvmpt2 
 |-  ( ( n e. Z /\ -u B e. _V ) -> ( ( n e. Z |-> -u B ) ` n ) = -u B )
58 55 57 mpan2 
 |-  ( n e. Z -> ( ( n e. Z |-> -u B ) ` n ) = -u B )
59 58 adantl 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( n e. Z |-> -u B ) ` n ) = -u B )
60 59 eqeq1d 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> -u B ) ` n ) = r <-> -u B = r ) )
61 52 54 60 3bitr4d 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ n e. Z ) -> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) )
62 61 ralrimiva 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> A. n e. Z ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) )
63 27 nfeq1 
 |-  F/ n ( ( n e. Z |-> B ) ` m ) = -u r
64 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> -u B ) ` m )
65 64 nfeq1 
 |-  F/ n ( ( n e. Z |-> -u B ) ` m ) = r
66 63 65 nfbi 
 |-  F/ n ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r )
67 nfv 
 |-  F/ m ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r )
68 fveqeq2 
 |-  ( m = n -> ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> B ) ` n ) = -u r ) )
69 fveqeq2 
 |-  ( m = n -> ( ( ( n e. Z |-> -u B ) ` m ) = r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) )
70 68 69 bibi12d 
 |-  ( m = n -> ( ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) <-> ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) ) )
71 66 67 70 cbvralw 
 |-  ( A. m e. Z ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) <-> A. n e. Z ( ( ( n e. Z |-> B ) ` n ) = -u r <-> ( ( n e. Z |-> -u B ) ` n ) = r ) )
72 62 71 sylibr 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> A. m e. Z ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) )
73 72 r19.21bi 
 |-  ( ( ( ( ph /\ x e. A ) /\ r e. RR ) /\ m e. Z ) -> ( ( ( n e. Z |-> B ) ` m ) = -u r <-> ( ( n e. Z |-> -u B ) ` m ) = r ) )
74 73 rexbidva 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) )
75 21 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> B ) Fn Z )
76 fvelrnb 
 |-  ( ( n e. Z |-> B ) Fn Z -> ( -u r e. ran ( n e. Z |-> B ) <-> E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r ) )
77 75 76 syl 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( -u r e. ran ( n e. Z |-> B ) <-> E. m e. Z ( ( n e. Z |-> B ) ` m ) = -u r ) )
78 7 renegcld 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> -u B e. RR )
79 78 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> -u B ) : Z --> RR )
80 79 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> -u B ) : Z --> RR )
81 80 ffnd 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( n e. Z |-> -u B ) Fn Z )
82 fvelrnb 
 |-  ( ( n e. Z |-> -u B ) Fn Z -> ( r e. ran ( n e. Z |-> -u B ) <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) )
83 81 82 syl 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( r e. ran ( n e. Z |-> -u B ) <-> E. m e. Z ( ( n e. Z |-> -u B ) ` m ) = r ) )
84 74 77 83 3bitr4d 
 |-  ( ( ( ph /\ x e. A ) /\ r e. RR ) -> ( -u r e. ran ( n e. Z |-> B ) <-> r e. ran ( n e. Z |-> -u B ) ) )
85 84 pm5.32da 
 |-  ( ( ph /\ x e. A ) -> ( ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) <-> ( r e. RR /\ r e. ran ( n e. Z |-> -u B ) ) ) )
86 79 frnd 
 |-  ( ( ph /\ x e. A ) -> ran ( n e. Z |-> -u B ) C_ RR )
87 86 sseld 
 |-  ( ( ph /\ x e. A ) -> ( r e. ran ( n e. Z |-> -u B ) -> r e. RR ) )
88 87 pm4.71rd 
 |-  ( ( ph /\ x e. A ) -> ( r e. ran ( n e. Z |-> -u B ) <-> ( r e. RR /\ r e. ran ( n e. Z |-> -u B ) ) ) )
89 85 88 bitr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( r e. RR /\ -u r e. ran ( n e. Z |-> B ) ) <-> r e. ran ( n e. Z |-> -u B ) ) )
90 44 89 syl5bb 
 |-  ( ( ph /\ x e. A ) -> ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) )
91 90 alrimiv 
 |-  ( ( ph /\ x e. A ) -> A. r ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) )
92 nfrab1 
 |-  F/_ r { r e. RR | -u r e. ran ( n e. Z |-> B ) }
93 nfcv 
 |-  F/_ r ran ( n e. Z |-> -u B )
94 92 93 cleqf 
 |-  ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } = ran ( n e. Z |-> -u B ) <-> A. r ( r e. { r e. RR | -u r e. ran ( n e. Z |-> B ) } <-> r e. ran ( n e. Z |-> -u B ) ) )
95 91 94 sylibr 
 |-  ( ( ph /\ x e. A ) -> { r e. RR | -u r e. ran ( n e. Z |-> B ) } = ran ( n e. Z |-> -u B ) )
96 95 supeq1d 
 |-  ( ( ph /\ x e. A ) -> sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) = sup ( ran ( n e. Z |-> -u B ) , RR , < ) )
97 96 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u sup ( { r e. RR | -u r e. ran ( n e. Z |-> B ) } , RR , < ) = -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) )
98 43 97 eqtrd 
 |-  ( ( ph /\ x e. A ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) )
99 98 mpteq2dva 
 |-  ( ph -> ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) )
100 2 99 eqtrid 
 |-  ( ph -> G = ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) )
101 ltso 
 |-  < Or RR
102 101 supex 
 |-  sup ( ran ( n e. Z |-> -u B ) , RR , < ) e. _V
103 102 a1i 
 |-  ( ( ph /\ x e. A ) -> sup ( ran ( n e. Z |-> -u B ) , RR , < ) e. _V )
104 eqid 
 |-  ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) = ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) )
105 5 anassrs 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. RR )
106 105 4 mbfneg 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> -u B ) e. MblFn )
107 5 renegcld 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> -u B e. RR )
108 renegcl 
 |-  ( y e. RR -> -u y e. RR )
109 108 ad2antrl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> -u y e. RR )
110 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> y e. RR )
111 7 adantlr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> B e. RR )
112 110 111 lenegd 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. RR ) /\ n e. Z ) -> ( y <_ B <-> -u B <_ -u y ) )
113 112 ralbidva 
 |-  ( ( ( ph /\ x e. A ) /\ y e. RR ) -> ( A. n e. Z y <_ B <-> A. n e. Z -u B <_ -u y ) )
114 113 biimpd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. RR ) -> ( A. n e. Z y <_ B -> A. n e. Z -u B <_ -u y ) )
115 114 impr 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> A. n e. Z -u B <_ -u y )
116 brralrspcev 
 |-  ( ( -u y e. RR /\ A. n e. Z -u B <_ -u y ) -> E. z e. RR A. n e. Z -u B <_ z )
117 109 115 116 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ A. n e. Z y <_ B ) ) -> E. z e. RR A. n e. Z -u B <_ z )
118 6 117 rexlimddv 
 |-  ( ( ph /\ x e. A ) -> E. z e. RR A. n e. Z -u B <_ z )
119 1 104 3 106 107 118 mbfsup 
 |-  ( ph -> ( x e. A |-> sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) e. MblFn )
120 103 119 mbfneg 
 |-  ( ph -> ( x e. A |-> -u sup ( ran ( n e. Z |-> -u B ) , RR , < ) ) e. MblFn )
121 100 120 eqeltrd 
 |-  ( ph -> G e. MblFn )