Metamath Proof Explorer

Theorem smflimsuplem4

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem4.1 ⊢ Ⅎ 𝑛 𝜑
smflimsuplem4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsuplem4.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsuplem4.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsuplem4.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimsuplem4.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
smflimsuplem4.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
smflimsuplem4.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
smflimsuplem4.i ⊢ ( 𝜑 → 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐻 ‘ 𝑛 ) )
smflimsuplem4.c ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
Assertion smflimsuplem4 ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 smflimsuplem4.1 ⊢ Ⅎ 𝑛 𝜑
2 smflimsuplem4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 smflimsuplem4.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 smflimsuplem4.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5 smflimsuplem4.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
6 smflimsuplem4.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
7 smflimsuplem4.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
8 smflimsuplem4.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
9 smflimsuplem4.i ⊢ ( 𝜑 → 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐻 ‘ 𝑛 ) )
10 smflimsuplem4.c ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
11 nfv ⊢ Ⅎ 𝑚 𝜑
12 3 8 eluzelz2d ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
14 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
15 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
16 11 2 12 3 13 14 15 limsupequzmpt ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑆 ∈ SAlg )
18 3 8 uzssd2 ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
19 18 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑚 ∈ 𝑍 )
20 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
21 19 20 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
22 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
23 17 21 22 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
24 3 6 7 19 smflimsuplem1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝐻 ‘ 𝑚 ) ⊆ dom ( 𝐹 ‘ 𝑚 ) )
25 9 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐻 ‘ 𝑛 ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
27 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐻 ‘ 𝑛 ) = ( 𝐻 ‘ 𝑚 ) )
28 27 dmeqd ⊢ ( 𝑛 = 𝑚 → dom ( 𝐻 ‘ 𝑛 ) = dom ( 𝐻 ‘ 𝑚 ) )
29 28 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ dom ( 𝐻 ‘ 𝑛 ) ↔ 𝑥 ∈ dom ( 𝐻 ‘ 𝑚 ) ) )
30 25 26 29 eliind ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ dom ( 𝐻 ‘ 𝑚 ) )
31 24 30 sseldd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
32 23 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
33 32 rexrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ* )
34 11 12 13 33 limsupvaluzmpt ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = inf ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) , ℝ* , < ) )
35 16 34 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = inf ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) , ℝ* , < ) )
36 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
38 36 37 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
39 7 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ) )
40 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
41 40 mptex ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V )
43 39 42 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
44 38 43 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
45 44 dmeqd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝐻 ‘ 𝑛 ) = dom ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
46 xrltso ⊢ < Or ℝ*
47 46 supex ⊢ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ V
48 eqid ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
49 47 48 dmmpti ⊢ dom ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝐸 ‘ 𝑛 )
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝐸 ‘ 𝑛 ) )
51 45 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝐻 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑛 ) )
52 1 51 iineq2d ⊢ ( 𝜑 → ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐻 ‘ 𝑛 ) = ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐸 ‘ 𝑛 ) )
53 9 52 eleqtrd ⊢ ( 𝜑 → 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐸 ‘ 𝑛 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐸 ‘ 𝑛 ) )
55 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐸 ‘ 𝑛 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
56 54 37 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) )
57 47 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ V )
58 44 57 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
59 56 58 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
60 eqid ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
61 3 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
62 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
63 61 62 uzn0d ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
64 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
65 64 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
66 65 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
67 66 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
68 63 67 iinexd ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
70 60 69 rabexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
71 38 70 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
72 6 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
73 38 71 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
74 56 73 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
75 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↔ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
76 74 75 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
77 76 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
78 59 77 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
79 1 59 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
80 nfv ⊢ Ⅎ 𝑘 𝜑
81 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
82 81 mpteq1d ⊢ ( 𝑛 = 𝑘 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
83 82 rneqd ⊢ ( 𝑛 = 𝑘 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
84 83 supeq1d ⊢ ( 𝑛 = 𝑘 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
85 nfv ⊢ Ⅎ 𝑚 ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) )
86 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑛 ∈ ℤ )
87 86 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑛 ∈ ℤ )
88 simpr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑘 = ( 𝑛 + 1 ) )
89 87 peano2zd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ( 𝑛 + 1 ) ∈ ℤ )
90 88 89 eqeltrd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑘 ∈ ℤ )
91 87 zred ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑛 ∈ ℝ )
92 90 zred ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑘 ∈ ℝ )
93 91 ltp1d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑛 < ( 𝑛 + 1 ) )
94 88 eqcomd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ( 𝑛 + 1 ) = 𝑘 )
95 93 94 breqtrd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑛 < 𝑘 )
96 91 92 95 ltled ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑛 ≤ 𝑘 )
97 62 87 90 96 eluzd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) )
98 uzss ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑛 ) )
99 97 98 syl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑛 ) )
100 fvexd ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
101 85 99 100 rnmptss2 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
102 101 3adant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
103 nfv ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
104 eqid ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
105 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
106 38 105 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
107 13 uztrn2 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
108 107 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
109 106 108 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
110 103 104 109 rnmptssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ℝ )
111 ressxr ⊢ ℝ ⊆ ℝ*
112 111 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ℝ ⊆ ℝ* )
113 110 112 sstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ℝ* )
114 113 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ℝ* )
115 supxrss ⊢ ( ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⊆ ℝ* ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ≤ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
116 102 114 115 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 = ( 𝑛 + 1 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ≤ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
117 3 fvexi ⊢ 𝑍 ∈ V
118 117 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
119 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ∈ V )
120 fvexd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ∈ V )
121 1 37 ssdf ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
122 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ∈ V )
123 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) )
124 1 12 13 118 18 119 120 121 122 123 climeldmeqmpt ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
125 10 124 mpbid ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
126 79 125 eqeltrrd ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ dom ⇝ )
127 1 80 12 13 77 84 116 126 climinf2mpt ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ⇝ inf ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) , ℝ* , < ) )
128 79 127 eqbrtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ inf ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) , ℝ* , < ) )
129 1 12 13 78 128 climreclmpt ⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) , ℝ* , < ) ∈ ℝ )
130 35 129 eqeltrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )