MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfsup Structured version   Visualization version   GIF version

Theorem mbfsup 24566
Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, 𝐵(𝑛, 𝑥) is a function of both 𝑛 and 𝑥, since it is an 𝑛-indexed sequence of functions on 𝑥. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)
Hypotheses
Ref Expression
mbfsup.1 𝑍 = (ℤ𝑀)
mbfsup.2 𝐺 = (𝑥𝐴 ↦ sup(ran (𝑛𝑍𝐵), ℝ, < ))
mbfsup.3 (𝜑𝑀 ∈ ℤ)
mbfsup.4 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵) ∈ MblFn)
mbfsup.5 ((𝜑 ∧ (𝑛𝑍𝑥𝐴)) → 𝐵 ∈ ℝ)
mbfsup.6 ((𝜑𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝐵𝑦)
Assertion
Ref Expression
mbfsup (𝜑𝐺 ∈ MblFn)
Distinct variable groups:   𝑥,𝑛,𝑦,𝐴   𝑦,𝐵   𝜑,𝑛,𝑥,𝑦   𝑛,𝑍,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑛)   𝐺(𝑥,𝑦,𝑛)   𝑀(𝑥,𝑦,𝑛)

Proof of Theorem mbfsup
Dummy variables 𝑚 𝑧 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfsup.5 . . . . . . . 8 ((𝜑 ∧ (𝑛𝑍𝑥𝐴)) → 𝐵 ∈ ℝ)
21anassrs 471 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
32an32s 652 . . . . . 6 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → 𝐵 ∈ ℝ)
43fmpttd 6937 . . . . 5 ((𝜑𝑥𝐴) → (𝑛𝑍𝐵):𝑍⟶ℝ)
54frnd 6558 . . . 4 ((𝜑𝑥𝐴) → ran (𝑛𝑍𝐵) ⊆ ℝ)
6 mbfsup.3 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
7 uzid 12458 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
86, 7syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ𝑀))
9 mbfsup.1 . . . . . . . . 9 𝑍 = (ℤ𝑀)
108, 9eleqtrrdi 2849 . . . . . . . 8 (𝜑𝑀𝑍)
1110adantr 484 . . . . . . 7 ((𝜑𝑥𝐴) → 𝑀𝑍)
12 eqid 2737 . . . . . . . 8 (𝑛𝑍𝐵) = (𝑛𝑍𝐵)
1312, 3dmmptd 6528 . . . . . . 7 ((𝜑𝑥𝐴) → dom (𝑛𝑍𝐵) = 𝑍)
1411, 13eleqtrrd 2841 . . . . . 6 ((𝜑𝑥𝐴) → 𝑀 ∈ dom (𝑛𝑍𝐵))
1514ne0d 4255 . . . . 5 ((𝜑𝑥𝐴) → dom (𝑛𝑍𝐵) ≠ ∅)
16 dm0rn0 5799 . . . . . 6 (dom (𝑛𝑍𝐵) = ∅ ↔ ran (𝑛𝑍𝐵) = ∅)
1716necon3bii 2993 . . . . 5 (dom (𝑛𝑍𝐵) ≠ ∅ ↔ ran (𝑛𝑍𝐵) ≠ ∅)
1815, 17sylib 221 . . . 4 ((𝜑𝑥𝐴) → ran (𝑛𝑍𝐵) ≠ ∅)
19 mbfsup.6 . . . . 5 ((𝜑𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝐵𝑦)
204ffnd 6551 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑛𝑍𝐵) Fn 𝑍)
21 breq1 5061 . . . . . . . . 9 (𝑧 = ((𝑛𝑍𝐵)‘𝑚) → (𝑧𝑦 ↔ ((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦))
2221ralrn 6912 . . . . . . . 8 ((𝑛𝑍𝐵) Fn 𝑍 → (∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦 ↔ ∀𝑚𝑍 ((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦))
2320, 22syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦 ↔ ∀𝑚𝑍 ((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦))
24 nffvmpt1 6733 . . . . . . . . . 10 𝑛((𝑛𝑍𝐵)‘𝑚)
25 nfcv 2904 . . . . . . . . . 10 𝑛
26 nfcv 2904 . . . . . . . . . 10 𝑛𝑦
2724, 25, 26nfbr 5105 . . . . . . . . 9 𝑛((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦
28 nfv 1922 . . . . . . . . 9 𝑚((𝑛𝑍𝐵)‘𝑛) ≤ 𝑦
29 fveq2 6722 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑛𝑍𝐵)‘𝑚) = ((𝑛𝑍𝐵)‘𝑛))
3029breq1d 5068 . . . . . . . . 9 (𝑚 = 𝑛 → (((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦 ↔ ((𝑛𝑍𝐵)‘𝑛) ≤ 𝑦))
3127, 28, 30cbvralw 3354 . . . . . . . 8 (∀𝑚𝑍 ((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛𝑍 ((𝑛𝑍𝐵)‘𝑛) ≤ 𝑦)
32 simpr 488 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → 𝑛𝑍)
3312fvmpt2 6834 . . . . . . . . . . 11 ((𝑛𝑍𝐵 ∈ ℝ) → ((𝑛𝑍𝐵)‘𝑛) = 𝐵)
3432, 3, 33syl2anc 587 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → ((𝑛𝑍𝐵)‘𝑛) = 𝐵)
3534breq1d 5068 . . . . . . . . 9 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → (((𝑛𝑍𝐵)‘𝑛) ≤ 𝑦𝐵𝑦))
3635ralbidva 3117 . . . . . . . 8 ((𝜑𝑥𝐴) → (∀𝑛𝑍 ((𝑛𝑍𝐵)‘𝑛) ≤ 𝑦 ↔ ∀𝑛𝑍 𝐵𝑦))
3731, 36syl5bb 286 . . . . . . 7 ((𝜑𝑥𝐴) → (∀𝑚𝑍 ((𝑛𝑍𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛𝑍 𝐵𝑦))
3823, 37bitrd 282 . . . . . 6 ((𝜑𝑥𝐴) → (∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦 ↔ ∀𝑛𝑍 𝐵𝑦))
3938rexbidv 3221 . . . . 5 ((𝜑𝑥𝐴) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝐵𝑦))
4019, 39mpbird 260 . . . 4 ((𝜑𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦)
415, 18, 40suprcld 11800 . . 3 ((𝜑𝑥𝐴) → sup(ran (𝑛𝑍𝐵), ℝ, < ) ∈ ℝ)
42 mbfsup.2 . . 3 𝐺 = (𝑥𝐴 ↦ sup(ran (𝑛𝑍𝐵), ℝ, < ))
4341, 42fmptd 6936 . 2 (𝜑𝐺:𝐴⟶ℝ)
44 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → 𝑥𝐴)
45 ltso 10918 . . . . . . . . . . . . . 14 < Or ℝ
4645supex 9084 . . . . . . . . . . . . 13 sup(ran (𝑛𝑍𝐵), ℝ, < ) ∈ V
4742fvmpt2 6834 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ sup(ran (𝑛𝑍𝐵), ℝ, < ) ∈ V) → (𝐺𝑥) = sup(ran (𝑛𝑍𝐵), ℝ, < ))
4844, 46, 47sylancl 589 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (𝐺𝑥) = sup(ran (𝑛𝑍𝐵), ℝ, < ))
4948breq2d 5070 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (𝑡 < (𝐺𝑥) ↔ 𝑡 < sup(ran (𝑛𝑍𝐵), ℝ, < )))
505, 18, 403jca 1130 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ran (𝑛𝑍𝐵) ⊆ ℝ ∧ ran (𝑛𝑍𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦))
5150adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (ran (𝑛𝑍𝐵) ⊆ ℝ ∧ ran (𝑛𝑍𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦))
52 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → 𝑡 ∈ ℝ)
53 suprlub 11801 . . . . . . . . . . . 12 (((ran (𝑛𝑍𝐵) ⊆ ℝ ∧ ran (𝑛𝑍𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛𝑍𝐵)𝑧𝑦) ∧ 𝑡 ∈ ℝ) → (𝑡 < sup(ran (𝑛𝑍𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛𝑍𝐵)𝑡 < 𝑧))
5451, 52, 53syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (𝑡 < sup(ran (𝑛𝑍𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛𝑍𝐵)𝑡 < 𝑧))
5520adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (𝑛𝑍𝐵) Fn 𝑍)
56 breq2 5062 . . . . . . . . . . . . . 14 (𝑧 = ((𝑛𝑍𝐵)‘𝑚) → (𝑡 < 𝑧𝑡 < ((𝑛𝑍𝐵)‘𝑚)))
5756rexrn 6911 . . . . . . . . . . . . 13 ((𝑛𝑍𝐵) Fn 𝑍 → (∃𝑧 ∈ ran (𝑛𝑍𝐵)𝑡 < 𝑧 ↔ ∃𝑚𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑚)))
5855, 57syl 17 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (∃𝑧 ∈ ran (𝑛𝑍𝐵)𝑡 < 𝑧 ↔ ∃𝑚𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑚)))
59 nfcv 2904 . . . . . . . . . . . . . . 15 𝑛𝑡
60 nfcv 2904 . . . . . . . . . . . . . . 15 𝑛 <
6159, 60, 24nfbr 5105 . . . . . . . . . . . . . 14 𝑛 𝑡 < ((𝑛𝑍𝐵)‘𝑚)
62 nfv 1922 . . . . . . . . . . . . . 14 𝑚 𝑡 < ((𝑛𝑍𝐵)‘𝑛)
6329breq2d 5070 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑡 < ((𝑛𝑍𝐵)‘𝑚) ↔ 𝑡 < ((𝑛𝑍𝐵)‘𝑛)))
6461, 62, 63cbvrexw 3355 . . . . . . . . . . . . 13 (∃𝑚𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑚) ↔ ∃𝑛𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑛))
6512fvmpt2i 6833 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → ((𝑛𝑍𝐵)‘𝑛) = ( I ‘𝐵))
66 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
6766fvmpt2i 6833 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → ((𝑥𝐴𝐵)‘𝑥) = ( I ‘𝐵))
6867adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = ( I ‘𝐵))
6968eqcomd 2743 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → ( I ‘𝐵) = ((𝑥𝐴𝐵)‘𝑥))
7065, 69sylan9eqr 2800 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → ((𝑛𝑍𝐵)‘𝑛) = ((𝑥𝐴𝐵)‘𝑥))
7170breq2d 5070 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → (𝑡 < ((𝑛𝑍𝐵)‘𝑛) ↔ 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7271rexbidva 3220 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (∃𝑛𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑛) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7372adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (∃𝑛𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑛) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7464, 73syl5bb 286 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (∃𝑚𝑍 𝑡 < ((𝑛𝑍𝐵)‘𝑚) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7558, 74bitrd 282 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (∃𝑧 ∈ ran (𝑛𝑍𝐵)𝑡 < 𝑧 ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7649, 54, 753bitrd 308 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥𝐴) → (𝑡 < (𝐺𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
7776ralrimiva 3105 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ) → ∀𝑥𝐴 (𝑡 < (𝐺𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)))
78 nfv 1922 . . . . . . . . . 10 𝑧(𝑡 < (𝐺𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥))
79 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑡
80 nfcv 2904 . . . . . . . . . . . 12 𝑥 <
81 nfmpt1 5158 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 ↦ sup(ran (𝑛𝑍𝐵), ℝ, < ))
8242, 81nfcxfr 2902 . . . . . . . . . . . . 13 𝑥𝐺
83 nfcv 2904 . . . . . . . . . . . . 13 𝑥𝑧
8482, 83nffv 6732 . . . . . . . . . . . 12 𝑥(𝐺𝑧)
8579, 80, 84nfbr 5105 . . . . . . . . . . 11 𝑥 𝑡 < (𝐺𝑧)
86 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑍
87 nffvmpt1 6733 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝐵)‘𝑧)
8879, 80, 87nfbr 5105 . . . . . . . . . . . 12 𝑥 𝑡 < ((𝑥𝐴𝐵)‘𝑧)
8986, 88nfrex 3233 . . . . . . . . . . 11 𝑥𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)
9085, 89nfbi 1911 . . . . . . . . . 10 𝑥(𝑡 < (𝐺𝑧) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧))
91 fveq2 6722 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
9291breq2d 5070 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑡 < (𝐺𝑥) ↔ 𝑡 < (𝐺𝑧)))
93 fveq2 6722 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝐵)‘𝑥) = ((𝑥𝐴𝐵)‘𝑧))
9493breq2d 5070 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑡 < ((𝑥𝐴𝐵)‘𝑥) ↔ 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
9594rexbidv 3221 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
9692, 95bibi12d 349 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝑡 < (𝐺𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)) ↔ (𝑡 < (𝐺𝑧) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
9778, 90, 96cbvralw 3354 . . . . . . . . 9 (∀𝑥𝐴 (𝑡 < (𝐺𝑥) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑥)) ↔ ∀𝑧𝐴 (𝑡 < (𝐺𝑧) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
9877, 97sylib 221 . . . . . . . 8 ((𝜑𝑡 ∈ ℝ) → ∀𝑧𝐴 (𝑡 < (𝐺𝑧) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
9998r19.21bi 3130 . . . . . . 7 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → (𝑡 < (𝐺𝑧) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
10043adantr 484 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ) → 𝐺:𝐴⟶ℝ)
101100ffvelrnda 6909 . . . . . . . 8 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → (𝐺𝑧) ∈ ℝ)
102 rexr 10884 . . . . . . . . . 10 (𝑡 ∈ ℝ → 𝑡 ∈ ℝ*)
103102ad2antlr 727 . . . . . . . . 9 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → 𝑡 ∈ ℝ*)
104 elioopnf 13036 . . . . . . . . 9 (𝑡 ∈ ℝ* → ((𝐺𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺𝑧) ∈ ℝ ∧ 𝑡 < (𝐺𝑧))))
105103, 104syl 17 . . . . . . . 8 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺𝑧) ∈ ℝ ∧ 𝑡 < (𝐺𝑧))))
106101, 105mpbirand 707 . . . . . . 7 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < (𝐺𝑧)))
107103adantr 484 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) ∧ 𝑛𝑍) → 𝑡 ∈ ℝ*)
108 elioopnf 13036 . . . . . . . . . 10 (𝑡 ∈ ℝ* → (((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥𝐴𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
109107, 108syl 17 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) ∧ 𝑛𝑍) → (((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥𝐴𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
1102fmpttd 6937 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵):𝐴⟶ℝ)
111110ffvelrnda 6909 . . . . . . . . . . . 12 (((𝜑𝑛𝑍) ∧ 𝑧𝐴) → ((𝑥𝐴𝐵)‘𝑧) ∈ ℝ)
112111biantrurd 536 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑧𝐴) → (𝑡 < ((𝑥𝐴𝐵)‘𝑧) ↔ (((𝑥𝐴𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
113112an32s 652 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑛𝑍) → (𝑡 < ((𝑥𝐴𝐵)‘𝑧) ↔ (((𝑥𝐴𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
114113adantllr 719 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) ∧ 𝑛𝑍) → (𝑡 < ((𝑥𝐴𝐵)‘𝑧) ↔ (((𝑥𝐴𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥𝐴𝐵)‘𝑧))))
115109, 114bitr4d 285 . . . . . . . 8 ((((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) ∧ 𝑛𝑍) → (((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
116115rexbidva 3220 . . . . . . 7 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → (∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛𝑍 𝑡 < ((𝑥𝐴𝐵)‘𝑧)))
11799, 106, 1163bitr4d 314 . . . . . 6 (((𝜑𝑡 ∈ ℝ) ∧ 𝑧𝐴) → ((𝐺𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞)))
118117pm5.32da 582 . . . . 5 ((𝜑𝑡 ∈ ℝ) → ((𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
11943ffnd 6551 . . . . . . 7 (𝜑𝐺 Fn 𝐴)
120119adantr 484 . . . . . 6 ((𝜑𝑡 ∈ ℝ) → 𝐺 Fn 𝐴)
121 elpreima 6883 . . . . . 6 (𝐺 Fn 𝐴 → (𝑧 ∈ (𝐺 “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑡(,)+∞))))
122120, 121syl 17 . . . . 5 ((𝜑𝑡 ∈ ℝ) → (𝑧 ∈ (𝐺 “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐺𝑧) ∈ (𝑡(,)+∞))))
123 eliun 4913 . . . . . 6 (𝑧 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛𝑍 𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)))
124110ffnd 6551 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵) Fn 𝐴)
125 elpreima 6883 . . . . . . . . . 10 ((𝑥𝐴𝐵) Fn 𝐴 → (𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
126124, 125syl 17 . . . . . . . . 9 ((𝜑𝑛𝑍) → (𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
127126rexbidva 3220 . . . . . . . 8 (𝜑 → (∃𝑛𝑍 𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛𝑍 (𝑧𝐴 ∧ ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
128127adantr 484 . . . . . . 7 ((𝜑𝑡 ∈ ℝ) → (∃𝑛𝑍 𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛𝑍 (𝑧𝐴 ∧ ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
129 r19.42v 3268 . . . . . . 7 (∃𝑛𝑍 (𝑧𝐴 ∧ ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞)))
130128, 129bitrdi 290 . . . . . 6 ((𝜑𝑡 ∈ ℝ) → (∃𝑛𝑍 𝑧 ∈ ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
131123, 130syl5bb 286 . . . . 5 ((𝜑𝑡 ∈ ℝ) → (𝑧 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ↔ (𝑧𝐴 ∧ ∃𝑛𝑍 ((𝑥𝐴𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
132118, 122, 1313bitr4d 314 . . . 4 ((𝜑𝑡 ∈ ℝ) → (𝑧 ∈ (𝐺 “ (𝑡(,)+∞)) ↔ 𝑧 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞))))
133132eqrdv 2735 . . 3 ((𝜑𝑡 ∈ ℝ) → (𝐺 “ (𝑡(,)+∞)) = 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)))
134 zex 12190 . . . . . . 7 ℤ ∈ V
135 uzssz 12464 . . . . . . 7 (ℤ𝑀) ⊆ ℤ
136 ssdomg 8679 . . . . . . 7 (ℤ ∈ V → ((ℤ𝑀) ⊆ ℤ → (ℤ𝑀) ≼ ℤ))
137134, 135, 136mp2 9 . . . . . 6 (ℤ𝑀) ≼ ℤ
1389, 137eqbrtri 5079 . . . . 5 𝑍 ≼ ℤ
139 znnen 15778 . . . . 5 ℤ ≈ ℕ
140 domentr 8692 . . . . 5 ((𝑍 ≼ ℤ ∧ ℤ ≈ ℕ) → 𝑍 ≼ ℕ)
141138, 139, 140mp2an 692 . . . 4 𝑍 ≼ ℕ
142 mbfsup.4 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵) ∈ MblFn)
143 mbfima 24532 . . . . . . 7 (((𝑥𝐴𝐵) ∈ MblFn ∧ (𝑥𝐴𝐵):𝐴⟶ℝ) → ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
144142, 110, 143syl2anc 587 . . . . . 6 ((𝜑𝑛𝑍) → ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
145144ralrimiva 3105 . . . . 5 (𝜑 → ∀𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
146145adantr 484 . . . 4 ((𝜑𝑡 ∈ ℝ) → ∀𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
147 iunmbl2 24459 . . . 4 ((𝑍 ≼ ℕ ∧ ∀𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol) → 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
148141, 146, 147sylancr 590 . . 3 ((𝜑𝑡 ∈ ℝ) → 𝑛𝑍 ((𝑥𝐴𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
149133, 148eqeltrd 2838 . 2 ((𝜑𝑡 ∈ ℝ) → (𝐺 “ (𝑡(,)+∞)) ∈ dom vol)
15043, 149ismbf3d 24556 1 (𝜑𝐺 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3413  wss 3871  c0 4242   ciun 4909   class class class wbr 5058  cmpt 5140   I cid 5459  ccnv 5555  dom cdm 5556  ran crn 5557  cima 5559   Fn wfn 6380  wf 6381  cfv 6385  (class class class)co 7218  cen 8628  cdom 8629  supcsup 9061  cr 10733  +∞cpnf 10869  *cxr 10871   < clt 10872  cle 10873  cn 11835  cz 12181  cuz 12443  (,)cioo 12940  volcvol 24365  MblFncmbf 24516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-inf2 9261  ax-cc 10054  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811  ax-pre-sup 10812
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-disj 5024  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-of 7474  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-2o 8208  df-oadd 8211  df-omul 8212  df-er 8396  df-map 8515  df-pm 8516  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-sup 9063  df-inf 9064  df-oi 9131  df-dju 9522  df-card 9560  df-acn 9563  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-div 11495  df-nn 11836  df-2 11898  df-3 11899  df-n0 12096  df-z 12182  df-uz 12444  df-q 12550  df-rp 12592  df-xadd 12710  df-ioo 12944  df-ioc 12945  df-ico 12946  df-icc 12947  df-fz 13101  df-fzo 13244  df-fl 13372  df-seq 13580  df-exp 13641  df-hash 13902  df-cj 14667  df-re 14668  df-im 14669  df-sqrt 14803  df-abs 14804  df-clim 15054  df-rlim 15055  df-sum 15255  df-xmet 20361  df-met 20362  df-ovol 24366  df-vol 24367  df-mbf 24521
This theorem is referenced by:  mbfinf  24567  mbflimsup  24568
  Copyright terms: Public domain W3C validator