Metamath Proof Explorer


Theorem mbflimsup

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)

Ref Expression
Hypotheses mbflimsup.1 𝑍 = ( ℤ𝑀 )
mbflimsup.2 𝐺 = ( 𝑥𝐴 ↦ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) )
mbflimsup.h 𝐻 = ( 𝑚 ∈ ℝ ↦ sup ( ( ( ( 𝑛𝑍𝐵 ) “ ( 𝑚 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
mbflimsup.3 ( 𝜑𝑀 ∈ ℤ )
mbflimsup.4 ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ )
mbflimsup.5 ( ( 𝜑𝑛𝑍 ) → ( 𝑥𝐴𝐵 ) ∈ MblFn )
mbflimsup.6 ( ( 𝜑 ∧ ( 𝑛𝑍𝑥𝐴 ) ) → 𝐵 ∈ ℝ )
Assertion mbflimsup ( 𝜑𝐺 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbflimsup.1 𝑍 = ( ℤ𝑀 )
2 mbflimsup.2 𝐺 = ( 𝑥𝐴 ↦ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) )
3 mbflimsup.h 𝐻 = ( 𝑚 ∈ ℝ ↦ sup ( ( ( ( 𝑛𝑍𝐵 ) “ ( 𝑚 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
4 mbflimsup.3 ( 𝜑𝑀 ∈ ℤ )
5 mbflimsup.4 ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ )
6 mbflimsup.5 ( ( 𝜑𝑛𝑍 ) → ( 𝑥𝐴𝐵 ) ∈ MblFn )
7 mbflimsup.6 ( ( 𝜑 ∧ ( 𝑛𝑍𝑥𝐴 ) ) → 𝐵 ∈ ℝ )
8 1 fvexi 𝑍 ∈ V
9 8 mptex ( 𝑛𝑍𝐵 ) ∈ V
10 9 a1i ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍𝐵 ) ∈ V )
11 uzssz ( ℤ𝑀 ) ⊆ ℤ
12 1 11 eqsstri 𝑍 ⊆ ℤ
13 zssre ℤ ⊆ ℝ
14 12 13 sstri 𝑍 ⊆ ℝ
15 14 a1i ( ( 𝜑𝑥𝐴 ) → 𝑍 ⊆ ℝ )
16 1 uzsup ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
17 4 16 syl ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
18 17 adantr ( ( 𝜑𝑥𝐴 ) → sup ( 𝑍 , ℝ* , < ) = +∞ )
19 3 10 15 18 limsupval2 ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) = inf ( ( 𝐻𝑍 ) , ℝ* , < ) )
20 imassrn ( 𝐻𝑍 ) ⊆ ran 𝐻
21 4 adantr ( ( 𝜑𝑥𝐴 ) → 𝑀 ∈ ℤ )
22 7 anass1rs ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℝ )
23 22 fmpttd ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ )
24 5 ltpnfd ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) < +∞ )
25 3 1 limsupgre ( ( 𝑀 ∈ ℤ ∧ ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) < +∞ ) → 𝐻 : ℝ ⟶ ℝ )
26 21 23 24 25 syl3anc ( ( 𝜑𝑥𝐴 ) → 𝐻 : ℝ ⟶ ℝ )
27 26 frnd ( ( 𝜑𝑥𝐴 ) → ran 𝐻 ⊆ ℝ )
28 20 27 sstrid ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) ⊆ ℝ )
29 26 fdmd ( ( 𝜑𝑥𝐴 ) → dom 𝐻 = ℝ )
30 29 ineq1d ( ( 𝜑𝑥𝐴 ) → ( dom 𝐻𝑍 ) = ( ℝ ∩ 𝑍 ) )
31 sseqin2 ( 𝑍 ⊆ ℝ ↔ ( ℝ ∩ 𝑍 ) = 𝑍 )
32 14 31 mpbi ( ℝ ∩ 𝑍 ) = 𝑍
33 30 32 eqtrdi ( ( 𝜑𝑥𝐴 ) → ( dom 𝐻𝑍 ) = 𝑍 )
34 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
35 4 34 syl ( 𝜑𝑀 ∈ ( ℤ𝑀 ) )
36 35 1 eleqtrrdi ( 𝜑𝑀𝑍 )
37 36 adantr ( ( 𝜑𝑥𝐴 ) → 𝑀𝑍 )
38 37 ne0d ( ( 𝜑𝑥𝐴 ) → 𝑍 ≠ ∅ )
39 33 38 eqnetrd ( ( 𝜑𝑥𝐴 ) → ( dom 𝐻𝑍 ) ≠ ∅ )
40 imadisj ( ( 𝐻𝑍 ) = ∅ ↔ ( dom 𝐻𝑍 ) = ∅ )
41 40 necon3bii ( ( 𝐻𝑍 ) ≠ ∅ ↔ ( dom 𝐻𝑍 ) ≠ ∅ )
42 39 41 sylibr ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) ≠ ∅ )
43 5 leidd ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) )
44 22 rexrd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℝ* )
45 44 fmpttd ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* )
46 5 rexrd ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ* )
47 3 limsuple ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* ∧ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ* ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ↔ ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
48 15 45 46 47 syl3anc ( ( 𝜑𝑥𝐴 ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ↔ ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
49 43 48 mpbid ( ( 𝜑𝑥𝐴 ) → ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) )
50 ssralv ( 𝑍 ⊆ ℝ → ( ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) → ∀ 𝑦𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
51 14 49 50 mpsyl ( ( 𝜑𝑥𝐴 ) → ∀ 𝑦𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) )
52 3 limsupgf 𝐻 : ℝ ⟶ ℝ*
53 ffn ( 𝐻 : ℝ ⟶ ℝ*𝐻 Fn ℝ )
54 52 53 ax-mp 𝐻 Fn ℝ
55 breq2 ( 𝑧 = ( 𝐻𝑦 ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ↔ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
56 55 ralima ( ( 𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ ) → ( ∀ 𝑧 ∈ ( 𝐻𝑍 ) ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ↔ ∀ 𝑦𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
57 54 15 56 sylancr ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑧 ∈ ( 𝐻𝑍 ) ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ↔ ∀ 𝑦𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑦 ) ) )
58 51 57 mpbird ( ( 𝜑𝑥𝐴 ) → ∀ 𝑧 ∈ ( 𝐻𝑍 ) ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 )
59 breq1 ( 𝑦 = ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) → ( 𝑦𝑧 ↔ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ) )
60 59 ralbidv ( 𝑦 = ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) → ( ∀ 𝑧 ∈ ( 𝐻𝑍 ) 𝑦𝑧 ↔ ∀ 𝑧 ∈ ( 𝐻𝑍 ) ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ) )
61 60 rspcev ( ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ ∧ ∀ 𝑧 ∈ ( 𝐻𝑍 ) ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻𝑍 ) 𝑦𝑧 )
62 5 58 61 syl2anc ( ( 𝜑𝑥𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻𝑍 ) 𝑦𝑧 )
63 infxrre ( ( ( 𝐻𝑍 ) ⊆ ℝ ∧ ( 𝐻𝑍 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻𝑍 ) 𝑦𝑧 ) → inf ( ( 𝐻𝑍 ) , ℝ* , < ) = inf ( ( 𝐻𝑍 ) , ℝ , < ) )
64 28 42 62 63 syl3anc ( ( 𝜑𝑥𝐴 ) → inf ( ( 𝐻𝑍 ) , ℝ* , < ) = inf ( ( 𝐻𝑍 ) , ℝ , < ) )
65 df-ima ( 𝐻𝑍 ) = ran ( 𝐻𝑍 )
66 26 feqmptd ( ( 𝜑𝑥𝐴 ) → 𝐻 = ( 𝑖 ∈ ℝ ↦ ( 𝐻𝑖 ) ) )
67 66 reseq1d ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) = ( ( 𝑖 ∈ ℝ ↦ ( 𝐻𝑖 ) ) ↾ 𝑍 ) )
68 resmpt ( 𝑍 ⊆ ℝ → ( ( 𝑖 ∈ ℝ ↦ ( 𝐻𝑖 ) ) ↾ 𝑍 ) = ( 𝑖𝑍 ↦ ( 𝐻𝑖 ) ) )
69 14 68 ax-mp ( ( 𝑖 ∈ ℝ ↦ ( 𝐻𝑖 ) ) ↾ 𝑍 ) = ( 𝑖𝑍 ↦ ( 𝐻𝑖 ) )
70 67 69 eqtrdi ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) = ( 𝑖𝑍 ↦ ( 𝐻𝑖 ) ) )
71 14 sseli ( 𝑖𝑍𝑖 ∈ ℝ )
72 ffvelrn ( ( 𝐻 : ℝ ⟶ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝐻𝑖 ) ∈ ℝ )
73 26 71 72 syl2an ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝐻𝑖 ) ∈ ℝ )
74 73 rexrd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝐻𝑖 ) ∈ ℝ* )
75 simplll ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝜑 )
76 1 uztrn2 ( ( 𝑖𝑍𝑛 ∈ ( ℤ𝑖 ) ) → 𝑛𝑍 )
77 76 adantll ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝑛𝑍 )
78 simpllr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝑥𝐴 )
79 75 77 78 7 syl12anc ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝐵 ∈ ℝ )
80 79 fmpttd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) : ( ℤ𝑖 ) ⟶ ℝ )
81 80 frnd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ⊆ ℝ )
82 eqid ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) = ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 )
83 82 79 dmmptd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → dom ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) = ( ℤ𝑖 ) )
84 simpr ( ( 𝜑𝑖𝑍 ) → 𝑖𝑍 )
85 84 1 eleqtrdi ( ( 𝜑𝑖𝑍 ) → 𝑖 ∈ ( ℤ𝑀 ) )
86 eluzelz ( 𝑖 ∈ ( ℤ𝑀 ) → 𝑖 ∈ ℤ )
87 85 86 syl ( ( 𝜑𝑖𝑍 ) → 𝑖 ∈ ℤ )
88 87 adantlr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ℤ )
89 uzid ( 𝑖 ∈ ℤ → 𝑖 ∈ ( ℤ𝑖 ) )
90 ne0i ( 𝑖 ∈ ( ℤ𝑖 ) → ( ℤ𝑖 ) ≠ ∅ )
91 88 89 90 3syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ℤ𝑖 ) ≠ ∅ )
92 83 91 eqnetrd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → dom ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ )
93 dm0rn0 ( dom ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) = ∅ ↔ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) = ∅ )
94 93 necon3bii ( dom ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ ↔ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ )
95 92 94 sylib ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ )
96 85 adantlr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ( ℤ𝑀 ) )
97 uzss ( 𝑖 ∈ ( ℤ𝑀 ) → ( ℤ𝑖 ) ⊆ ( ℤ𝑀 ) )
98 96 97 syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ℤ𝑖 ) ⊆ ( ℤ𝑀 ) )
99 98 1 sseqtrrdi ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ℤ𝑖 ) ⊆ 𝑍 )
100 73 leidd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝐻𝑖 ) ≤ ( 𝐻𝑖 ) )
101 14 a1i ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → 𝑍 ⊆ ℝ )
102 45 adantr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* )
103 simpr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → 𝑖𝑍 )
104 14 103 sselid ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ℝ )
105 3 limsupgle ( ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* ) ∧ 𝑖 ∈ ℝ ∧ ( 𝐻𝑖 ) ∈ ℝ* ) → ( ( 𝐻𝑖 ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
106 101 102 104 74 105 syl211anc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ( 𝐻𝑖 ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
107 100 106 mpbid ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
108 ssralv ( ( ℤ𝑖 ) ⊆ 𝑍 → ( ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) → ∀ 𝑘 ∈ ( ℤ𝑖 ) ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
109 99 107 108 sylc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑘 ∈ ( ℤ𝑖 ) ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
110 99 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ℤ𝑖 ) ⊆ 𝑍 )
111 110 resmptd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( 𝑛𝑍𝐵 ) ↾ ( ℤ𝑖 ) ) = ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) )
112 111 fveq1d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( ( 𝑛𝑍𝐵 ) ↾ ( ℤ𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) )
113 fvres ( 𝑘 ∈ ( ℤ𝑖 ) → ( ( ( 𝑛𝑍𝐵 ) ↾ ( ℤ𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) )
114 113 adantl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( ( 𝑛𝑍𝐵 ) ↾ ( ℤ𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) )
115 112 114 eqtr3d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) )
116 115 breq1d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ↔ ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
117 eluzle ( 𝑘 ∈ ( ℤ𝑖 ) → 𝑖𝑘 )
118 117 adantl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → 𝑖𝑘 )
119 biimt ( 𝑖𝑘 → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ↔ ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
120 118 119 syl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ↔ ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
121 116 120 bitrd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ↔ ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
122 121 ralbidva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑖 ) ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑖 ) ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) ) )
123 109 122 mpbird ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑘 ∈ ( ℤ𝑖 ) ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) )
124 ffn ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) : ( ℤ𝑖 ) ⟶ ℝ → ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) Fn ( ℤ𝑖 ) )
125 breq1 ( 𝑧 = ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) → ( 𝑧 ≤ ( 𝐻𝑖 ) ↔ ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
126 125 ralrn ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) Fn ( ℤ𝑖 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑖 ) ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
127 80 124 126 3syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑖 ) ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻𝑖 ) ) )
128 123 127 mpbird ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) )
129 brralrspcev ( ( ( 𝐻𝑖 ) ∈ ℝ ∧ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 )
130 73 128 129 syl2anc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 )
131 81 95 130 suprcld ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ )
132 131 rexrd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ* )
133 81 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ⊆ ℝ )
134 95 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ )
135 130 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 )
136 12 sseli ( 𝑘𝑍𝑘 ∈ ℤ )
137 eluz ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ𝑖 ) ↔ 𝑖𝑘 ) )
138 88 136 137 syl2an ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘𝑍 ) → ( 𝑘 ∈ ( ℤ𝑖 ) ↔ 𝑖𝑘 ) )
139 138 biimprd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘𝑍 ) → ( 𝑖𝑘𝑘 ∈ ( ℤ𝑖 ) ) )
140 139 impr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → 𝑘 ∈ ( ℤ𝑖 ) )
141 140 115 syldan ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) )
142 80 adantr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) : ( ℤ𝑖 ) ⟶ ℝ )
143 142 124 syl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) Fn ( ℤ𝑖 ) )
144 fnfvelrn ( ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) Fn ( ℤ𝑖 ) ∧ 𝑘 ∈ ( ℤ𝑖 ) ) → ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) )
145 143 140 144 syl2anc ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) )
146 141 145 eqeltrrd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) )
147 133 134 135 146 suprubd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ ( 𝑘𝑍𝑖𝑘 ) ) → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
148 147 expr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) ∧ 𝑘𝑍 ) → ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
149 148 ralrimiva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
150 3 limsupgle ( ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* ) ∧ 𝑖 ∈ ℝ ∧ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ* ) → ( ( 𝐻𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) )
151 101 102 104 132 150 syl211anc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ( 𝐻𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑘𝑍 ( 𝑖𝑘 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) )
152 149 151 mpbird ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝐻𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
153 suprleub ( ( ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 ) ∧ ( 𝐻𝑖 ) ∈ ℝ ) → ( sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) ) )
154 81 95 130 73 153 syl31anc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻𝑖 ) ) )
155 128 154 mpbird ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻𝑖 ) )
156 74 132 152 155 xrletrid ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( 𝐻𝑖 ) = sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
157 156 mpteq2dva ( ( 𝜑𝑥𝐴 ) → ( 𝑖𝑍 ↦ ( 𝐻𝑖 ) ) = ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
158 70 157 eqtrd ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) = ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
159 158 rneqd ( ( 𝜑𝑥𝐴 ) → ran ( 𝐻𝑍 ) = ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
160 65 159 syl5eq ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑍 ) = ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
161 160 infeq1d ( ( 𝜑𝑥𝐴 ) → inf ( ( 𝐻𝑍 ) , ℝ , < ) = inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) )
162 19 64 161 3eqtrd ( ( 𝜑𝑥𝐴 ) → ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) = inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) )
163 162 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ) = ( 𝑥𝐴 ↦ inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) )
164 2 163 syl5eq ( 𝜑𝐺 = ( 𝑥𝐴 ↦ inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) )
165 eqid ( 𝑥𝐴 ↦ inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) = ( 𝑥𝐴 ↦ inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) )
166 eqid ( ℤ𝑖 ) = ( ℤ𝑖 )
167 eqid ( 𝑥𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) = ( 𝑥𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
168 simpll ( ( ( 𝜑𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝜑 )
169 76 adantll ( ( ( 𝜑𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → 𝑛𝑍 )
170 168 169 6 syl2anc ( ( ( 𝜑𝑖𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑖 ) ) → ( 𝑥𝐴𝐵 ) ∈ MblFn )
171 simpll ( ( ( 𝜑𝑖𝑍 ) ∧ ( 𝑛 ∈ ( ℤ𝑖 ) ∧ 𝑥𝐴 ) ) → 𝜑 )
172 76 ad2ant2lr ( ( ( 𝜑𝑖𝑍 ) ∧ ( 𝑛 ∈ ( ℤ𝑖 ) ∧ 𝑥𝐴 ) ) → 𝑛𝑍 )
173 simprr ( ( ( 𝜑𝑖𝑍 ) ∧ ( 𝑛 ∈ ( ℤ𝑖 ) ∧ 𝑥𝐴 ) ) → 𝑥𝐴 )
174 171 172 173 7 syl12anc ( ( ( 𝜑𝑖𝑍 ) ∧ ( 𝑛 ∈ ( ℤ𝑖 ) ∧ 𝑥𝐴 ) ) → 𝐵 ∈ ℝ )
175 79 ralrimiva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵 ∈ ℝ )
176 breq1 ( 𝑧 = 𝐵 → ( 𝑧𝑦𝐵𝑦 ) )
177 82 176 ralrnmptw ( ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵 ∈ ℝ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 ↔ ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵𝑦 ) )
178 175 177 syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 ↔ ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵𝑦 ) )
179 178 rexbidv ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) 𝑧𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵𝑦 ) )
180 130 179 mpbid ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵𝑦 )
181 180 an32s ( ( ( 𝜑𝑖𝑍 ) ∧ 𝑥𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ𝑖 ) 𝐵𝑦 )
182 166 167 87 170 174 181 mbfsup ( ( 𝜑𝑖𝑍 ) → ( 𝑥𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ∈ MblFn )
183 131 an32s ( ( ( 𝜑𝑖𝑍 ) ∧ 𝑥𝐴 ) → sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ )
184 183 anasss ( ( 𝜑 ∧ ( 𝑖𝑍𝑥𝐴 ) ) → sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ )
185 3 limsuple ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ* ∧ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ* ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ↔ ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) ) )
186 15 45 46 185 syl3anc ( ( 𝜑𝑥𝐴 ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ↔ ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) ) )
187 43 186 mpbid ( ( 𝜑𝑥𝐴 ) → ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) )
188 ssralv ( 𝑍 ⊆ ℝ → ( ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) → ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) ) )
189 14 187 188 mpsyl ( ( 𝜑𝑥𝐴 ) → ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) )
190 156 breq2d ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑖𝑍 ) → ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) ↔ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
191 190 ralbidva ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ ( 𝐻𝑖 ) ↔ ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
192 189 191 mpbid ( ( 𝜑𝑥𝐴 ) → ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
193 breq1 ( 𝑦 = ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) → ( 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
194 193 ralbidv ( 𝑦 = ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) → ( ∀ 𝑖𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) )
195 194 rspcev ( ( ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ∈ ℝ ∧ ∀ 𝑖𝑍 ( lim sup ‘ ( 𝑛𝑍𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
196 5 192 195 syl2anc ( ( 𝜑𝑥𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
197 1 165 4 182 184 196 mbfinf ( 𝜑 → ( 𝑥𝐴 ↦ inf ( ran ( 𝑖𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) ∈ MblFn )
198 164 197 eqeltrd ( 𝜑𝐺 ∈ MblFn )