This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝐻 : ℝ ⟶ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝐻 ‘ 𝑖 ) ∈ ℝ )
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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 “ 𝑍 ) = 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 eqtrid ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 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 )