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 )