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

Theorem mbflimsup 25714
Description: The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
Hypotheses
Ref Expression
mbflimsup.1 𝑍 = (ℤ𝑀)
mbflimsup.2 𝐺 = (𝑥𝐴 ↦ (lim sup‘(𝑛𝑍𝐵)))
mbflimsup.h 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛𝑍𝐵) “ (𝑚[,)+∞)) ∩ ℝ*), ℝ*, < ))
mbflimsup.3 (𝜑𝑀 ∈ ℤ)
mbflimsup.4 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) ∈ ℝ)
mbflimsup.5 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵) ∈ MblFn)
mbflimsup.6 ((𝜑 ∧ (𝑛𝑍𝑥𝐴)) → 𝐵 ∈ ℝ)
Assertion
Ref Expression
mbflimsup (𝜑𝐺 ∈ MblFn)
Distinct variable groups:   𝑥,𝑛,𝐴   𝐵,𝑚   𝜑,𝑛,𝑥   𝑚,𝑀   𝑚,𝑛,𝑥,𝑍
Allowed substitution hints:   𝜑(𝑚)   𝐴(𝑚)   𝐵(𝑥,𝑛)   𝐺(𝑥,𝑚,𝑛)   𝐻(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑛)

Proof of Theorem mbflimsup
Dummy variables 𝑖 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbflimsup.2 . . 3 𝐺 = (𝑥𝐴 ↦ (lim sup‘(𝑛𝑍𝐵)))
2 mbflimsup.h . . . . . 6 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛𝑍𝐵) “ (𝑚[,)+∞)) ∩ ℝ*), ℝ*, < ))
3 mbflimsup.1 . . . . . . . . 9 𝑍 = (ℤ𝑀)
43fvexi 6920 . . . . . . . 8 𝑍 ∈ V
54mptex 7242 . . . . . . 7 (𝑛𝑍𝐵) ∈ V
65a1i 11 . . . . . 6 ((𝜑𝑥𝐴) → (𝑛𝑍𝐵) ∈ V)
7 uzssz 12896 . . . . . . . . 9 (ℤ𝑀) ⊆ ℤ
83, 7eqsstri 4029 . . . . . . . 8 𝑍 ⊆ ℤ
9 zssre 12617 . . . . . . . 8 ℤ ⊆ ℝ
108, 9sstri 4004 . . . . . . 7 𝑍 ⊆ ℝ
1110a1i 11 . . . . . 6 ((𝜑𝑥𝐴) → 𝑍 ⊆ ℝ)
12 mbflimsup.3 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
133uzsup 13899 . . . . . . . 8 (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞)
1412, 13syl 17 . . . . . . 7 (𝜑 → sup(𝑍, ℝ*, < ) = +∞)
1514adantr 480 . . . . . 6 ((𝜑𝑥𝐴) → sup(𝑍, ℝ*, < ) = +∞)
162, 6, 11, 15limsupval2 15512 . . . . 5 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) = inf((𝐻𝑍), ℝ*, < ))
17 imassrn 6090 . . . . . . 7 (𝐻𝑍) ⊆ ran 𝐻
1812adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑀 ∈ ℤ)
19 mbflimsup.6 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑍𝑥𝐴)) → 𝐵 ∈ ℝ)
2019anass1rs 655 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → 𝐵 ∈ ℝ)
2120fmpttd 7134 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑛𝑍𝐵):𝑍⟶ℝ)
22 mbflimsup.4 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) ∈ ℝ)
2322ltpnfd 13160 . . . . . . . . 9 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) < +∞)
242, 3limsupgre 15513 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ (𝑛𝑍𝐵):𝑍⟶ℝ ∧ (lim sup‘(𝑛𝑍𝐵)) < +∞) → 𝐻:ℝ⟶ℝ)
2518, 21, 23, 24syl3anc 1370 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐻:ℝ⟶ℝ)
2625frnd 6744 . . . . . . 7 ((𝜑𝑥𝐴) → ran 𝐻 ⊆ ℝ)
2717, 26sstrid 4006 . . . . . 6 ((𝜑𝑥𝐴) → (𝐻𝑍) ⊆ ℝ)
2825fdmd 6746 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom 𝐻 = ℝ)
2928ineq1d 4226 . . . . . . . . 9 ((𝜑𝑥𝐴) → (dom 𝐻𝑍) = (ℝ ∩ 𝑍))
30 sseqin2 4230 . . . . . . . . . 10 (𝑍 ⊆ ℝ ↔ (ℝ ∩ 𝑍) = 𝑍)
3110, 30mpbi 230 . . . . . . . . 9 (ℝ ∩ 𝑍) = 𝑍
3229, 31eqtrdi 2790 . . . . . . . 8 ((𝜑𝑥𝐴) → (dom 𝐻𝑍) = 𝑍)
33 uzid 12890 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
3412, 33syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (ℤ𝑀))
3534, 3eleqtrrdi 2849 . . . . . . . . . 10 (𝜑𝑀𝑍)
3635adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑀𝑍)
3736ne0d 4347 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝑍 ≠ ∅)
3832, 37eqnetrd 3005 . . . . . . 7 ((𝜑𝑥𝐴) → (dom 𝐻𝑍) ≠ ∅)
39 imadisj 6099 . . . . . . . 8 ((𝐻𝑍) = ∅ ↔ (dom 𝐻𝑍) = ∅)
4039necon3bii 2990 . . . . . . 7 ((𝐻𝑍) ≠ ∅ ↔ (dom 𝐻𝑍) ≠ ∅)
4138, 40sylibr 234 . . . . . 6 ((𝜑𝑥𝐴) → (𝐻𝑍) ≠ ∅)
4222leidd 11826 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) ≤ (lim sup‘(𝑛𝑍𝐵)))
4320rexrd 11308 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑛𝑍) → 𝐵 ∈ ℝ*)
4443fmpttd 7134 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑛𝑍𝐵):𝑍⟶ℝ*)
4522rexrd 11308 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) ∈ ℝ*)
462limsuple 15510 . . . . . . . . . . 11 ((𝑍 ⊆ ℝ ∧ (𝑛𝑍𝐵):𝑍⟶ℝ* ∧ (lim sup‘(𝑛𝑍𝐵)) ∈ ℝ*) → ((lim sup‘(𝑛𝑍𝐵)) ≤ (lim sup‘(𝑛𝑍𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
4711, 44, 45, 46syl3anc 1370 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((lim sup‘(𝑛𝑍𝐵)) ≤ (lim sup‘(𝑛𝑍𝐵)) ↔ ∀𝑦 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
4842, 47mpbid 232 . . . . . . . . 9 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦))
49 ssralv 4063 . . . . . . . . 9 (𝑍 ⊆ ℝ → (∀𝑦 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦) → ∀𝑦𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
5010, 48, 49mpsyl 68 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑦𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦))
512limsupgf 15507 . . . . . . . . . 10 𝐻:ℝ⟶ℝ*
52 ffn 6736 . . . . . . . . . 10 (𝐻:ℝ⟶ℝ*𝐻 Fn ℝ)
5351, 52ax-mp 5 . . . . . . . . 9 𝐻 Fn ℝ
54 breq2 5151 . . . . . . . . . 10 (𝑧 = (𝐻𝑦) → ((lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧 ↔ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
5554ralima 7256 . . . . . . . . 9 ((𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ) → (∀𝑧 ∈ (𝐻𝑍)(lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧 ↔ ∀𝑦𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
5653, 11, 55sylancr 587 . . . . . . . 8 ((𝜑𝑥𝐴) → (∀𝑧 ∈ (𝐻𝑍)(lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧 ↔ ∀𝑦𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑦)))
5750, 56mpbird 257 . . . . . . 7 ((𝜑𝑥𝐴) → ∀𝑧 ∈ (𝐻𝑍)(lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧)
58 breq1 5150 . . . . . . . . 9 (𝑦 = (lim sup‘(𝑛𝑍𝐵)) → (𝑦𝑧 ↔ (lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧))
5958ralbidv 3175 . . . . . . . 8 (𝑦 = (lim sup‘(𝑛𝑍𝐵)) → (∀𝑧 ∈ (𝐻𝑍)𝑦𝑧 ↔ ∀𝑧 ∈ (𝐻𝑍)(lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧))
6059rspcev 3621 . . . . . . 7 (((lim sup‘(𝑛𝑍𝐵)) ∈ ℝ ∧ ∀𝑧 ∈ (𝐻𝑍)(lim sup‘(𝑛𝑍𝐵)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻𝑍)𝑦𝑧)
6122, 57, 60syl2anc 584 . . . . . 6 ((𝜑𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻𝑍)𝑦𝑧)
62 infxrre 13374 . . . . . 6 (((𝐻𝑍) ⊆ ℝ ∧ (𝐻𝑍) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐻𝑍)𝑦𝑧) → inf((𝐻𝑍), ℝ*, < ) = inf((𝐻𝑍), ℝ, < ))
6327, 41, 61, 62syl3anc 1370 . . . . 5 ((𝜑𝑥𝐴) → inf((𝐻𝑍), ℝ*, < ) = inf((𝐻𝑍), ℝ, < ))
64 df-ima 5701 . . . . . . 7 (𝐻𝑍) = ran (𝐻𝑍)
6525feqmptd 6976 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐻 = (𝑖 ∈ ℝ ↦ (𝐻𝑖)))
6665reseq1d 5998 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐻𝑍) = ((𝑖 ∈ ℝ ↦ (𝐻𝑖)) ↾ 𝑍))
67 resmpt 6056 . . . . . . . . . . 11 (𝑍 ⊆ ℝ → ((𝑖 ∈ ℝ ↦ (𝐻𝑖)) ↾ 𝑍) = (𝑖𝑍 ↦ (𝐻𝑖)))
6810, 67ax-mp 5 . . . . . . . . . 10 ((𝑖 ∈ ℝ ↦ (𝐻𝑖)) ↾ 𝑍) = (𝑖𝑍 ↦ (𝐻𝑖))
6966, 68eqtrdi 2790 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐻𝑍) = (𝑖𝑍 ↦ (𝐻𝑖)))
7010sseli 3990 . . . . . . . . . . . . 13 (𝑖𝑍𝑖 ∈ ℝ)
71 ffvelcdm 7100 . . . . . . . . . . . . 13 ((𝐻:ℝ⟶ℝ ∧ 𝑖 ∈ ℝ) → (𝐻𝑖) ∈ ℝ)
7225, 70, 71syl2an 596 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝐻𝑖) ∈ ℝ)
7372rexrd 11308 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝐻𝑖) ∈ ℝ*)
74 simplll 775 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝜑)
753uztrn2 12894 . . . . . . . . . . . . . . . . 17 ((𝑖𝑍𝑛 ∈ (ℤ𝑖)) → 𝑛𝑍)
7675adantll 714 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑛𝑍)
77 simpllr 776 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑥𝐴)
7874, 76, 77, 19syl12anc 837 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝐵 ∈ ℝ)
7978fmpttd 7134 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝑛 ∈ (ℤ𝑖) ↦ 𝐵):(ℤ𝑖)⟶ℝ)
8079frnd 6744 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ⊆ ℝ)
81 eqid 2734 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) = (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)
8281, 78dmmptd 6713 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → dom (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) = (ℤ𝑖))
83 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → 𝑖𝑍)
8483, 3eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑍) → 𝑖 ∈ (ℤ𝑀))
85 eluzelz 12885 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℤ)
8684, 85syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑍) → 𝑖 ∈ ℤ)
8786adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → 𝑖 ∈ ℤ)
88 uzid 12890 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℤ → 𝑖 ∈ (ℤ𝑖))
89 ne0i 4346 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (ℤ𝑖) → (ℤ𝑖) ≠ ∅)
9087, 88, 893syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (ℤ𝑖) ≠ ∅)
9182, 90eqnetrd 3005 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → dom (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅)
92 dm0rn0 5937 . . . . . . . . . . . . . . 15 (dom (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) = ∅)
9392necon3bii 2990 . . . . . . . . . . . . . 14 (dom (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅)
9491, 93sylib 218 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅)
9584adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → 𝑖 ∈ (ℤ𝑀))
96 uzss 12898 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → (ℤ𝑖) ⊆ (ℤ𝑀))
9795, 96syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (ℤ𝑖) ⊆ (ℤ𝑀))
9897, 3sseqtrrdi 4046 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (ℤ𝑖) ⊆ 𝑍)
9972leidd 11826 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝐻𝑖) ≤ (𝐻𝑖))
10010a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → 𝑍 ⊆ ℝ)
10144adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝑛𝑍𝐵):𝑍⟶ℝ*)
102 simpr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → 𝑖𝑍)
10310, 102sselid 3992 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → 𝑖 ∈ ℝ)
1042limsupgle 15509 . . . . . . . . . . . . . . . . . . 19 (((𝑍 ⊆ ℝ ∧ (𝑛𝑍𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ (𝐻𝑖) ∈ ℝ*) → ((𝐻𝑖) ≤ (𝐻𝑖) ↔ ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
105100, 101, 103, 73, 104syl211anc 1375 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ((𝐻𝑖) ≤ (𝐻𝑖) ↔ ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
10699, 105mpbid 232 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖)))
107 ssralv 4063 . . . . . . . . . . . . . . . . 17 ((ℤ𝑖) ⊆ 𝑍 → (∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖)) → ∀𝑘 ∈ (ℤ𝑖)(𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
10898, 106, 107sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑘 ∈ (ℤ𝑖)(𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖)))
10998adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (ℤ𝑖) ⊆ 𝑍)
110109resmptd 6059 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → ((𝑛𝑍𝐵) ↾ (ℤ𝑖)) = (𝑛 ∈ (ℤ𝑖) ↦ 𝐵))
111110fveq1d 6908 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (((𝑛𝑍𝐵) ↾ (ℤ𝑖))‘𝑘) = ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘))
112 fvres 6925 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (ℤ𝑖) → (((𝑛𝑍𝐵) ↾ (ℤ𝑖))‘𝑘) = ((𝑛𝑍𝐵)‘𝑘))
113112adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (((𝑛𝑍𝐵) ↾ (ℤ𝑖))‘𝑘) = ((𝑛𝑍𝐵)‘𝑘))
114111, 113eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) = ((𝑛𝑍𝐵)‘𝑘))
115114breq1d 5157 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖) ↔ ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖)))
116 eluzle 12888 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ𝑖) → 𝑖𝑘)
117116adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → 𝑖𝑘)
118 biimt 360 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑘 → (((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖) ↔ (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
119117, 118syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖) ↔ (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
120115, 119bitrd 279 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘 ∈ (ℤ𝑖)) → (((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖) ↔ (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
121120ralbidva 3173 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (∀𝑘 ∈ (ℤ𝑖)((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖) ↔ ∀𝑘 ∈ (ℤ𝑖)(𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ (𝐻𝑖))))
122108, 121mpbird 257 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑘 ∈ (ℤ𝑖)((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖))
123 ffn 6736 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵):(ℤ𝑖)⟶ℝ → (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) Fn (ℤ𝑖))
124 breq1 5150 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) → (𝑧 ≤ (𝐻𝑖) ↔ ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖)))
125124ralrn 7107 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵) Fn (ℤ𝑖) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖) ↔ ∀𝑘 ∈ (ℤ𝑖)((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖)))
12679, 123, 1253syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖) ↔ ∀𝑘 ∈ (ℤ𝑖)((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ≤ (𝐻𝑖)))
127122, 126mpbird 257 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖))
128 brralrspcev 5207 . . . . . . . . . . . . . 14 (((𝐻𝑖) ∈ ℝ ∧ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦)
12972, 127, 128syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦)
13080, 94, 129suprcld 12228 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ∈ ℝ)
131130rexrd 11308 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ∈ ℝ*)
13280adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ⊆ ℝ)
13394adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅)
134129adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦)
1358sseli 3990 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑍𝑘 ∈ ℤ)
136 eluz 12889 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑖) ↔ 𝑖𝑘))
13787, 135, 136syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘𝑍) → (𝑘 ∈ (ℤ𝑖) ↔ 𝑖𝑘))
138137biimprd 248 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘𝑍) → (𝑖𝑘𝑘 ∈ (ℤ𝑖)))
139138impr 454 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → 𝑘 ∈ (ℤ𝑖))
140139, 114syldan 591 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) = ((𝑛𝑍𝐵)‘𝑘))
14179adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → (𝑛 ∈ (ℤ𝑖) ↦ 𝐵):(ℤ𝑖)⟶ℝ)
142141, 123syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) Fn (ℤ𝑖))
143 fnfvelrn 7099 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ (ℤ𝑖) ↦ 𝐵) Fn (ℤ𝑖) ∧ 𝑘 ∈ (ℤ𝑖)) → ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵))
144142, 139, 143syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ((𝑛 ∈ (ℤ𝑖) ↦ 𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵))
145140, 144eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ((𝑛𝑍𝐵)‘𝑘) ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵))
146132, 133, 134, 145suprubd 12227 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ (𝑘𝑍𝑖𝑘)) → ((𝑛𝑍𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
147146expr 456 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐴) ∧ 𝑖𝑍) ∧ 𝑘𝑍) → (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
148147ralrimiva 3143 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
1492limsupgle 15509 . . . . . . . . . . . . 13 (((𝑍 ⊆ ℝ ∧ (𝑛𝑍𝐵):𝑍⟶ℝ*) ∧ 𝑖 ∈ ℝ ∧ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ∈ ℝ*) → ((𝐻𝑖) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))))
150100, 101, 103, 131, 149syl211anc 1375 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ((𝐻𝑖) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑘𝑍 (𝑖𝑘 → ((𝑛𝑍𝐵)‘𝑘) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))))
151148, 150mpbird 257 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝐻𝑖) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
152 suprleub 12231 . . . . . . . . . . . . 13 (((ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦) ∧ (𝐻𝑖) ∈ ℝ) → (sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖)))
15380, 94, 129, 72, 152syl31anc 1372 . . . . . . . . . . . 12 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻𝑖) ↔ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧 ≤ (𝐻𝑖)))
154127, 153mpbird 257 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ≤ (𝐻𝑖))
15573, 131, 151, 154xrletrid 13193 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (𝐻𝑖) = sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
156155mpteq2dva 5247 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑖𝑍 ↦ (𝐻𝑖)) = (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
15769, 156eqtrd 2774 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐻𝑍) = (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
158157rneqd 5951 . . . . . . 7 ((𝜑𝑥𝐴) → ran (𝐻𝑍) = ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
15964, 158eqtrid 2786 . . . . . 6 ((𝜑𝑥𝐴) → (𝐻𝑍) = ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
160159infeq1d 9514 . . . . 5 ((𝜑𝑥𝐴) → inf((𝐻𝑍), ℝ, < ) = inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < ))
16116, 63, 1603eqtrd 2778 . . . 4 ((𝜑𝑥𝐴) → (lim sup‘(𝑛𝑍𝐵)) = inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < ))
162161mpteq2dva 5247 . . 3 (𝜑 → (𝑥𝐴 ↦ (lim sup‘(𝑛𝑍𝐵))) = (𝑥𝐴 ↦ inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )))
1631, 162eqtrid 2786 . 2 (𝜑𝐺 = (𝑥𝐴 ↦ inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )))
164 eqid 2734 . . 3 (𝑥𝐴 ↦ inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) = (𝑥𝐴 ↦ inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < ))
165 eqid 2734 . . . 4 (ℤ𝑖) = (ℤ𝑖)
166 eqid 2734 . . . 4 (𝑥𝐴 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )) = (𝑥𝐴 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
167 simpll 767 . . . . 5 (((𝜑𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝜑)
16875adantll 714 . . . . 5 (((𝜑𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → 𝑛𝑍)
169 mbflimsup.5 . . . . 5 ((𝜑𝑛𝑍) → (𝑥𝐴𝐵) ∈ MblFn)
170167, 168, 169syl2anc 584 . . . 4 (((𝜑𝑖𝑍) ∧ 𝑛 ∈ (ℤ𝑖)) → (𝑥𝐴𝐵) ∈ MblFn)
171 simpll 767 . . . . 5 (((𝜑𝑖𝑍) ∧ (𝑛 ∈ (ℤ𝑖) ∧ 𝑥𝐴)) → 𝜑)
17275ad2ant2lr 748 . . . . 5 (((𝜑𝑖𝑍) ∧ (𝑛 ∈ (ℤ𝑖) ∧ 𝑥𝐴)) → 𝑛𝑍)
173 simprr 773 . . . . 5 (((𝜑𝑖𝑍) ∧ (𝑛 ∈ (ℤ𝑖) ∧ 𝑥𝐴)) → 𝑥𝐴)
174171, 172, 173, 19syl12anc 837 . . . 4 (((𝜑𝑖𝑍) ∧ (𝑛 ∈ (ℤ𝑖) ∧ 𝑥𝐴)) → 𝐵 ∈ ℝ)
17578ralrimiva 3143 . . . . . . . 8 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∀𝑛 ∈ (ℤ𝑖)𝐵 ∈ ℝ)
176 breq1 5150 . . . . . . . . 9 (𝑧 = 𝐵 → (𝑧𝑦𝐵𝑦))
17781, 176ralrnmptw 7113 . . . . . . . 8 (∀𝑛 ∈ (ℤ𝑖)𝐵 ∈ ℝ → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦 ↔ ∀𝑛 ∈ (ℤ𝑖)𝐵𝑦))
178175, 177syl 17 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦 ↔ ∀𝑛 ∈ (ℤ𝑖)𝐵𝑦))
179178rexbidv 3176 . . . . . 6 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵)𝑧𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ𝑖)𝐵𝑦))
180129, 179mpbid 232 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ𝑖)𝐵𝑦)
181180an32s 652 . . . 4 (((𝜑𝑖𝑍) ∧ 𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ (ℤ𝑖)𝐵𝑦)
182165, 166, 86, 170, 174, 181mbfsup 25712 . . 3 ((𝜑𝑖𝑍) → (𝑥𝐴 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )) ∈ MblFn)
183130an32s 652 . . . 4 (((𝜑𝑖𝑍) ∧ 𝑥𝐴) → sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ∈ ℝ)
184183anasss 466 . . 3 ((𝜑 ∧ (𝑖𝑍𝑥𝐴)) → sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ∈ ℝ)
1852limsuple 15510 . . . . . . . 8 ((𝑍 ⊆ ℝ ∧ (𝑛𝑍𝐵):𝑍⟶ℝ* ∧ (lim sup‘(𝑛𝑍𝐵)) ∈ ℝ*) → ((lim sup‘(𝑛𝑍𝐵)) ≤ (lim sup‘(𝑛𝑍𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖)))
18611, 44, 45, 185syl3anc 1370 . . . . . . 7 ((𝜑𝑥𝐴) → ((lim sup‘(𝑛𝑍𝐵)) ≤ (lim sup‘(𝑛𝑍𝐵)) ↔ ∀𝑖 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖)))
18742, 186mpbid 232 . . . . . 6 ((𝜑𝑥𝐴) → ∀𝑖 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖))
188 ssralv 4063 . . . . . 6 (𝑍 ⊆ ℝ → (∀𝑖 ∈ ℝ (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖) → ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖)))
18910, 187, 188mpsyl 68 . . . . 5 ((𝜑𝑥𝐴) → ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖))
190155breq2d 5159 . . . . . 6 (((𝜑𝑥𝐴) ∧ 𝑖𝑍) → ((lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖) ↔ (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
191190ralbidva 3173 . . . . 5 ((𝜑𝑥𝐴) → (∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ (𝐻𝑖) ↔ ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
192189, 191mpbid 232 . . . 4 ((𝜑𝑥𝐴) → ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
193 breq1 5150 . . . . . 6 (𝑦 = (lim sup‘(𝑛𝑍𝐵)) → (𝑦 ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ↔ (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
194193ralbidv 3175 . . . . 5 (𝑦 = (lim sup‘(𝑛𝑍𝐵)) → (∀𝑖𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ) ↔ ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )))
195194rspcev 3621 . . . 4 (((lim sup‘(𝑛𝑍𝐵)) ∈ ℝ ∧ ∀𝑖𝑍 (lim sup‘(𝑛𝑍𝐵)) ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )) → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
19622, 192, 195syl2anc 584 . . 3 ((𝜑𝑥𝐴) → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < ))
1973, 164, 12, 182, 184, 196mbfinf 25713 . 2 (𝜑 → (𝑥𝐴 ↦ inf(ran (𝑖𝑍 ↦ sup(ran (𝑛 ∈ (ℤ𝑖) ↦ 𝐵), ℝ, < )), ℝ, < )) ∈ MblFn)
198163, 197eqeltrd 2838 1 (𝜑𝐺 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cin 3961  wss 3962  c0 4338   class class class wbr 5147  cmpt 5230  dom cdm 5688  ran crn 5689  cres 5690  cima 5691   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  supcsup 9477  infcinf 9478  cr 11151  +∞cpnf 11289  *cxr 11291   < clt 11292  cle 11293  cz 12610  cuz 12875  [,)cico 13385  lim supclsp 15502  MblFncmbf 25662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cc 10472  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-omul 8509  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-rp 13032  df-xadd 13152  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-xmet 21374  df-met 21375  df-ovol 25512  df-vol 25513  df-mbf 25667
This theorem is referenced by:  mbflimlem  25715
  Copyright terms: Public domain W3C validator