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=ℤ≥M
mbfinf.2 ⊢G=x∈A⟼supran⁡n∈Z⟼Bℝ<
mbfinf.3 ⊢φ→M∈ℤ
mbfinf.4 ⊢φ∧n∈Z→x∈A⟼B∈MblFn
mbfinf.5 ⊢φ∧n∈Z∧x∈A→B∈ℝ
mbfinf.6 ⊢φ∧x∈A→∃y∈ℝ∀n∈Zy≤B
Assertion mbfinf ⊢φ→G∈MblFn

Proof

Step Hyp Ref Expression
1 mbfinf.1 ⊢Z=ℤ≥M
2 mbfinf.2 ⊢G=x∈A⟼supran⁡n∈Z⟼Bℝ<
3 mbfinf.3 ⊢φ→M∈ℤ
4 mbfinf.4 ⊢φ∧n∈Z→x∈A⟼B∈MblFn
5 mbfinf.5 ⊢φ∧n∈Z∧x∈A→B∈ℝ
6 mbfinf.6 ⊢φ∧x∈A→∃y∈ℝ∀n∈Zy≤B
7 5 anass1rs ⊢φ∧x∈A∧n∈Z→B∈ℝ
8 7 fmpttd ⊢φ∧x∈A→n∈Z⟼B:Z⟶ℝ
9 8 frnd ⊢φ∧x∈A→ran⁡n∈Z⟼B⊆ℝ
10 uzid ⊢M∈ℤ→M∈ℤ≥M
11 3 10 syl ⊢φ→M∈ℤ≥M
12 11 1 eleqtrrdi ⊢φ→M∈Z
13 12 adantr ⊢φ∧x∈A→M∈Z
14 eqid ⊢n∈Z⟼B=n∈Z⟼B
15 14 7 dmmptd ⊢φ∧x∈A→dom⁡n∈Z⟼B=Z
16 13 15 eleqtrrd ⊢φ∧x∈A→M∈dom⁡n∈Z⟼B
17 16 ne0d ⊢φ∧x∈A→dom⁡n∈Z⟼B≠∅
18 dm0rn0 ⊢dom⁡n∈Z⟼B=∅↔ran⁡n∈Z⟼B=∅
19 18 necon3bii ⊢dom⁡n∈Z⟼B≠∅↔ran⁡n∈Z⟼B≠∅
20 17 19 sylib ⊢φ∧x∈A→ran⁡n∈Z⟼B≠∅
21 8 ffnd ⊢φ∧x∈A→n∈Z⟼BFnZ
22 breq2 ⊢z=n∈Z⟼B⁡m→y≤z↔y≤n∈Z⟼B⁡m
23 22 ralrn ⊢n∈Z⟼BFnZ→∀z∈ran⁡n∈Z⟼By≤z↔∀m∈Zy≤n∈Z⟼B⁡m
24 21 23 syl ⊢φ∧x∈A→∀z∈ran⁡n∈Z⟼By≤z↔∀m∈Zy≤n∈Z⟼B⁡m
25 nfcv ⊢Ⅎ_ny
26 nfcv ⊢Ⅎ_n≤
27 nffvmpt1 ⊢Ⅎ_nn∈Z⟼B⁡m
28 25 26 27 nfbr ⊢Ⅎny≤n∈Z⟼B⁡m
29 nfv ⊢Ⅎmy≤n∈Z⟼B⁡n
30 fveq2 ⊢m=n→n∈Z⟼B⁡m=n∈Z⟼B⁡n
31 30 breq2d ⊢m=n→y≤n∈Z⟼B⁡m↔y≤n∈Z⟼B⁡n
32 28 29 31 cbvralw ⊢∀m∈Zy≤n∈Z⟼B⁡m↔∀n∈Zy≤n∈Z⟼B⁡n
33 simpr ⊢φ∧x∈A∧n∈Z→n∈Z
34 14 fvmpt2 ⊢n∈Z∧B∈ℝ→n∈Z⟼B⁡n=B
35 33 7 34 syl2anc ⊢φ∧x∈A∧n∈Z→n∈Z⟼B⁡n=B
36 35 breq2d ⊢φ∧x∈A∧n∈Z→y≤n∈Z⟼B⁡n↔y≤B
37 36 ralbidva ⊢φ∧x∈A→∀n∈Zy≤n∈Z⟼B⁡n↔∀n∈Zy≤B
38 32 37 bitrid ⊢φ∧x∈A→∀m∈Zy≤n∈Z⟼B⁡m↔∀n∈Zy≤B
39 24 38 bitrd ⊢φ∧x∈A→∀z∈ran⁡n∈Z⟼By≤z↔∀n∈Zy≤B
40 39 rexbidv ⊢φ∧x∈A→∃y∈ℝ∀z∈ran⁡n∈Z⟼By≤z↔∃y∈ℝ∀n∈Zy≤B
41 6 40 mpbird ⊢φ∧x∈A→∃y∈ℝ∀z∈ran⁡n∈Z⟼By≤z
42 infrenegsup ⊢ran⁡n∈Z⟼B⊆ℝ∧ran⁡n∈Z⟼B≠∅∧∃y∈ℝ∀z∈ran⁡n∈Z⟼By≤z→supran⁡n∈Z⟼Bℝ<=−supr∈ℝ|−r∈ran⁡n∈Z⟼Bℝ<
43 9 20 41 42 syl3anc ⊢φ∧x∈A→supran⁡n∈Z⟼Bℝ<=−supr∈ℝ|−r∈ran⁡n∈Z⟼Bℝ<
44 rabid ⊢r∈r∈ℝ|−r∈ran⁡n∈Z⟼B↔r∈ℝ∧−r∈ran⁡n∈Z⟼B
45 7 recnd ⊢φ∧x∈A∧n∈Z→B∈ℂ
46 45 adantlr ⊢φ∧x∈A∧r∈ℝ∧n∈Z→B∈ℂ
47 simplr ⊢φ∧x∈A∧r∈ℝ∧n∈Z→r∈ℝ
48 47 recnd ⊢φ∧x∈A∧r∈ℝ∧n∈Z→r∈ℂ
49 negcon2 ⊢B∈ℂ∧r∈ℂ→B=−r↔r=−B
50 46 48 49 syl2anc ⊢φ∧x∈A∧r∈ℝ∧n∈Z→B=−r↔r=−B
51 eqcom ⊢r=−B↔−B=r
52 50 51 bitrdi ⊢φ∧x∈A∧r∈ℝ∧n∈Z→B=−r↔−B=r
53 35 adantlr ⊢φ∧x∈A∧r∈ℝ∧n∈Z→n∈Z⟼B⁡n=B
54 53 eqeq1d ⊢φ∧x∈A∧r∈ℝ∧n∈Z→n∈Z⟼B⁡n=−r↔B=−r
55 negex ⊢−B∈V
56 eqid ⊢n∈Z⟼−B=n∈Z⟼−B
57 56 fvmpt2 ⊢n∈Z∧−B∈V→n∈Z⟼−B⁡n=−B
58 55 57 mpan2 ⊢n∈Z→n∈Z⟼−B⁡n=−B
59 58 adantl ⊢φ∧x∈A∧r∈ℝ∧n∈Z→n∈Z⟼−B⁡n=−B
60 59 eqeq1d ⊢φ∧x∈A∧r∈ℝ∧n∈Z→n∈Z⟼−B⁡n=r↔−B=r
61 52 54 60 3bitr4d ⊢φ∧x∈A∧r∈ℝ∧n∈Z→n∈Z⟼B⁡n=−r↔n∈Z⟼−B⁡n=r
62 61 ralrimiva ⊢φ∧x∈A∧r∈ℝ→∀n∈Zn∈Z⟼B⁡n=−r↔n∈Z⟼−B⁡n=r
63 27 nfeq1 ⊢Ⅎnn∈Z⟼B⁡m=−r
64 nffvmpt1 ⊢Ⅎ_nn∈Z⟼−B⁡m
65 64 nfeq1 ⊢Ⅎnn∈Z⟼−B⁡m=r
66 63 65 nfbi ⊢Ⅎnn∈Z⟼B⁡m=−r↔n∈Z⟼−B⁡m=r
67 nfv ⊢Ⅎmn∈Z⟼B⁡n=−r↔n∈Z⟼−B⁡n=r
68 fveqeq2 ⊢m=n→n∈Z⟼B⁡m=−r↔n∈Z⟼B⁡n=−r
69 fveqeq2 ⊢m=n→n∈Z⟼−B⁡m=r↔n∈Z⟼−B⁡n=r
70 68 69 bibi12d ⊢m=n→n∈Z⟼B⁡m=−r↔n∈Z⟼−B⁡m=r↔n∈Z⟼B⁡n=−r↔n∈Z⟼−B⁡n=r
71 66 67 70 cbvralw ⊢∀m∈Zn∈Z⟼B⁡m=−r↔n∈Z⟼−B⁡m=r↔∀n∈Zn∈Z⟼B⁡n=−r↔n∈Z⟼−B⁡n=r
72 62 71 sylibr ⊢φ∧x∈A∧r∈ℝ→∀m∈Zn∈Z⟼B⁡m=−r↔n∈Z⟼−B⁡m=r
73 72 r19.21bi ⊢φ∧x∈A∧r∈ℝ∧m∈Z→n∈Z⟼B⁡m=−r↔n∈Z⟼−B⁡m=r
74 73 rexbidva ⊢φ∧x∈A∧r∈ℝ→∃m∈Zn∈Z⟼B⁡m=−r↔∃m∈Zn∈Z⟼−B⁡m=r
75 21 adantr ⊢φ∧x∈A∧r∈ℝ→n∈Z⟼BFnZ
76 fvelrnb ⊢n∈Z⟼BFnZ→−r∈ran⁡n∈Z⟼B↔∃m∈Zn∈Z⟼B⁡m=−r
77 75 76 syl ⊢φ∧x∈A∧r∈ℝ→−r∈ran⁡n∈Z⟼B↔∃m∈Zn∈Z⟼B⁡m=−r
78 7 renegcld ⊢φ∧x∈A∧n∈Z→−B∈ℝ
79 78 fmpttd ⊢φ∧x∈A→n∈Z⟼−B:Z⟶ℝ
80 79 adantr ⊢φ∧x∈A∧r∈ℝ→n∈Z⟼−B:Z⟶ℝ
81 80 ffnd ⊢φ∧x∈A∧r∈ℝ→n∈Z⟼−BFnZ
82 fvelrnb ⊢n∈Z⟼−BFnZ→r∈ran⁡n∈Z⟼−B↔∃m∈Zn∈Z⟼−B⁡m=r
83 81 82 syl ⊢φ∧x∈A∧r∈ℝ→r∈ran⁡n∈Z⟼−B↔∃m∈Zn∈Z⟼−B⁡m=r
84 74 77 83 3bitr4d ⊢φ∧x∈A∧r∈ℝ→−r∈ran⁡n∈Z⟼B↔r∈ran⁡n∈Z⟼−B
85 84 pm5.32da ⊢φ∧x∈A→r∈ℝ∧−r∈ran⁡n∈Z⟼B↔r∈ℝ∧r∈ran⁡n∈Z⟼−B
86 79 frnd ⊢φ∧x∈A→ran⁡n∈Z⟼−B⊆ℝ
87 86 sseld ⊢φ∧x∈A→r∈ran⁡n∈Z⟼−B→r∈ℝ
88 87 pm4.71rd ⊢φ∧x∈A→r∈ran⁡n∈Z⟼−B↔r∈ℝ∧r∈ran⁡n∈Z⟼−B
89 85 88 bitr4d ⊢φ∧x∈A→r∈ℝ∧−r∈ran⁡n∈Z⟼B↔r∈ran⁡n∈Z⟼−B
90 44 89 bitrid ⊢φ∧x∈A→r∈r∈ℝ|−r∈ran⁡n∈Z⟼B↔r∈ran⁡n∈Z⟼−B
91 90 alrimiv ⊢φ∧x∈A→∀rr∈r∈ℝ|−r∈ran⁡n∈Z⟼B↔r∈ran⁡n∈Z⟼−B
92 nfrab1 ⊢Ⅎ_rr∈ℝ|−r∈ran⁡n∈Z⟼B
93 nfcv ⊢Ⅎ_rran⁡n∈Z⟼−B
94 92 93 cleqf ⊢r∈ℝ|−r∈ran⁡n∈Z⟼B=ran⁡n∈Z⟼−B↔∀rr∈r∈ℝ|−r∈ran⁡n∈Z⟼B↔r∈ran⁡n∈Z⟼−B
95 91 94 sylibr ⊢φ∧x∈A→r∈ℝ|−r∈ran⁡n∈Z⟼B=ran⁡n∈Z⟼−B
96 95 supeq1d ⊢φ∧x∈A→supr∈ℝ|−r∈ran⁡n∈Z⟼Bℝ<=supran⁡n∈Z⟼−Bℝ<
97 96 negeqd ⊢φ∧x∈A→−supr∈ℝ|−r∈ran⁡n∈Z⟼Bℝ<=−supran⁡n∈Z⟼−Bℝ<
98 43 97 eqtrd ⊢φ∧x∈A→supran⁡n∈Z⟼Bℝ<=−supran⁡n∈Z⟼−Bℝ<
99 98 mpteq2dva ⊢φ→x∈A⟼supran⁡n∈Z⟼Bℝ<=x∈A⟼−supran⁡n∈Z⟼−Bℝ<
100 2 99 eqtrid ⊢φ→G=x∈A⟼−supran⁡n∈Z⟼−Bℝ<
101 ltso ⊢<Orℝ
102 101 supex ⊢supran⁡n∈Z⟼−Bℝ<∈V
103 102 a1i ⊢φ∧x∈A→supran⁡n∈Z⟼−Bℝ<∈V
104 eqid ⊢x∈A⟼supran⁡n∈Z⟼−Bℝ<=x∈A⟼supran⁡n∈Z⟼−Bℝ<
105 5 anassrs ⊢φ∧n∈Z∧x∈A→B∈ℝ
106 105 4 mbfneg ⊢φ∧n∈Z→x∈A⟼−B∈MblFn
107 5 renegcld ⊢φ∧n∈Z∧x∈A→−B∈ℝ
108 renegcl ⊢y∈ℝ→−y∈ℝ
109 108 ad2antrl ⊢φ∧x∈A∧y∈ℝ∧∀n∈Zy≤B→−y∈ℝ
110 simplr ⊢φ∧x∈A∧y∈ℝ∧n∈Z→y∈ℝ
111 7 adantlr ⊢φ∧x∈A∧y∈ℝ∧n∈Z→B∈ℝ
112 110 111 lenegd ⊢φ∧x∈A∧y∈ℝ∧n∈Z→y≤B↔−B≤−y
113 112 ralbidva ⊢φ∧x∈A∧y∈ℝ→∀n∈Zy≤B↔∀n∈Z−B≤−y
114 113 biimpd ⊢φ∧x∈A∧y∈ℝ→∀n∈Zy≤B→∀n∈Z−B≤−y
115 114 impr ⊢φ∧x∈A∧y∈ℝ∧∀n∈Zy≤B→∀n∈Z−B≤−y
116 brralrspcev ⊢−y∈ℝ∧∀n∈Z−B≤−y→∃z∈ℝ∀n∈Z−B≤z
117 109 115 116 syl2anc ⊢φ∧x∈A∧y∈ℝ∧∀n∈Zy≤B→∃z∈ℝ∀n∈Z−B≤z
118 6 117 rexlimddv ⊢φ∧x∈A→∃z∈ℝ∀n∈Z−B≤z
119 1 104 3 106 107 118 mbfsup ⊢φ→x∈A⟼supran⁡n∈Z⟼−Bℝ<∈MblFn
120 103 119 mbfneg ⊢φ→x∈A⟼−supran⁡n∈Z⟼−Bℝ<∈MblFn
121 100 120 eqeltrd ⊢φ→G∈MblFn