Metamath Proof Explorer

Theorem smflimsuplem5

Description: H converges to the superior limit of F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 smflimsuplem5.a ⊢ Ⅎ 𝑛 𝜑
2 smflimsuplem5.b ⊢ Ⅎ 𝑚 𝜑
3 smflimsuplem5.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 smflimsuplem5.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 smflimsuplem5.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6 smflimsuplem5.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7 smflimsuplem5.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
8 smflimsuplem5.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
9 smflimsuplem5.r ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
10 smflimsuplem5.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
11 smflimsuplem5.x ⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) )
12 4 eleq2i ⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 12 biimpi ⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
14 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
15 13 14 syl ⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
16 15 4 sseqtrrdi ⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
17 10 16 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
19 nfcv ⊢ Ⅎ 𝑥 𝑍
20 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
21 19 20 nfmpt ⊢ Ⅎ 𝑥 ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
22 7 21 nfcxfr ⊢ Ⅎ 𝑥 𝐸
23 nfcv ⊢ Ⅎ 𝑥 𝑛
24 22 23 nffv ⊢ Ⅎ 𝑥 ( 𝐸 ‘ 𝑛 )
25 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
26 24 25 mptexf ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V )
28 8 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
29 18 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
30 29 fveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ‘ 𝑋 ) )
31 nfcv ⊢ Ⅎ 𝑦 ( 𝐸 ‘ 𝑛 )
32 nfcv ⊢ Ⅎ 𝑦 sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < )
33 nfcv ⊢ Ⅎ 𝑥 sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < )
34 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
35 34 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
36 35 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
37 36 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) )
38 24 31 32 33 37 cbvmptf ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑦 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) )
39 simpl ⊢ ( ( 𝑦 = 𝑋 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑦 = 𝑋 )
40 39 fveq2d ⊢ ( ( 𝑦 = 𝑋 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
41 40 mpteq2dva ⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
42 41 rneqd ⊢ ( 𝑦 = 𝑋 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
43 42 supeq1d ⊢ ( 𝑦 = 𝑋 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) )
44 43 eleq1d ⊢ ( 𝑦 = 𝑋 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ) )
45 uzss ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
46 iinss1 ⊢ ( ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑁 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
47 45 46 syl ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
49 11 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) )
50 48 49 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
51 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ ( ℤ≥ ‘ 𝑁 )
52 2 51 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
53 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
54 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
55 45 sselda ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
56 55 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
57 5 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑆 ∈ SAlg )
58 simpl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝜑 )
59 17 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑚 ∈ 𝑍 )
60 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
61 58 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
62 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
63 57 61 62 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
64 eliin ⊢ ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) ) )
65 11 64 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) ) )
66 11 65 mpbid ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
68 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) )
69 rspa ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
70 67 68 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
71 63 70 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )
72 54 56 71 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )
73 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑛 ∈ ℤ )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℤ )
75 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
76 fvex ⊢ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V
77 76 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V )
78 52 74 75 53 4 72 77 limsupequzmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
79 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
80 78 79 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
81 80 renepnfd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ≠ +∞ )
82 52 53 72 81 limsupubuzmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ≤ 𝑦 )
83 uzid2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
84 83 ne0d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
86 52 85 72 supxrre3rnmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ≤ 𝑦 ) )
87 82 86 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ )
88 44 50 87 elrabd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ } )
89 simpl ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑦 = 𝑥 )
90 89 fveq2d ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
91 90 mpteq2dva ⊢ ( 𝑦 = 𝑥 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
92 91 rneqd ⊢ ( 𝑦 = 𝑥 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
93 92 supeq1d ⊢ ( 𝑦 = 𝑥 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
94 93 eleq1d ⊢ ( 𝑦 = 𝑥 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
95 94 cbvrabv ⊢ { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
96 88 95 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
97 eqid ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
98 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
99 98 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
100 99 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
101 100 a1i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
102 84 101 iinexd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
103 102 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
104 97 103 rabexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
105 7 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
106 18 104 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
107 96 106 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ ( 𝐸 ‘ 𝑛 ) )
108 38 43 107 87 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ‘ 𝑋 ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) )
109 30 108 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) )
110 1 109 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ) )
111 4 eluzelz2 ⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ )
112 10 111 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
113 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
114 76 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V )
115 76 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V )
116 2 112 3 113 4 114 115 limsupequzmpt ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
117 116 9 eqeltrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
118 2 112 113 71 117 supcnvlimsupmpt ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
119 110 118 eqbrtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )