Metamath Proof Explorer

Theorem smflimsuplem8

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem8.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsuplem8.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsuplem8.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsuplem8.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimsuplem8.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
smflimsuplem8.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
smflimsuplem8.e ⊢ 𝐸 = ( 𝑘 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
smflimsuplem8.h ⊢ 𝐻 = ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑘 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
Assertion smflimsuplem8 ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem8.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smflimsuplem8.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smflimsuplem8.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smflimsuplem8.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smflimsuplem8.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
6 smflimsuplem8.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
7 smflimsuplem8.e ⊢ 𝐸 = ( 𝑘 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
8 smflimsuplem8.h ⊢ 𝐻 = ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑘 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
9 6 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
10 1 2 3 4 5 7 8 smflimsuplem7 ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
11 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
12 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
13 11 12 sylib ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
14 13 5 eleq2s ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
16 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
17 nfv ⊢ Ⅎ 𝑛 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) )
18 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
19 nfv ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
20 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
21 nfcv ⊢ Ⅎ 𝑚 𝑥
22 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
23 21 22 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
24 19 20 23 nf3an ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
25 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑀 ∈ ℤ )
26 25 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑀 ∈ ℤ )
27 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑆 ∈ SAlg )
28 27 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑆 ∈ SAlg )
29 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
30 29 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
31 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
32 31 5 eleq2s ⊢ ( 𝑥 ∈ 𝐷 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
33 fveq2 ⊢ ( 𝑚 = 𝑦 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑦 ) )
34 33 fveq1d ⊢ ( 𝑚 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) )
35 34 cbvmptv ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) )
36 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
37 36 fveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) )
38 37 cbvmptv ⊢ ( 𝑧 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) )
39 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
40 39 fveq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) )
41 40 cbvmptv ⊢ ( 𝑧 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑥 ) ) = ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) )
42 35 38 41 3eqtr2i ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) )
43 42 fveq2i ⊢ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) ) )
44 43 eleq1i ⊢ ( ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∈ ℝ )
45 32 44 sylib ⊢ ( 𝑥 ∈ 𝐷 → ( lim sup ‘ ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∈ ℝ )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∈ ℝ )
47 46 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim sup ‘ ( 𝑤 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∈ ℝ )
48 47 44 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
49 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑛 ∈ 𝑍 )
50 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
51 18 24 26 2 28 30 7 8 48 49 50 smflimsuplem5 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
52 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ℤ≥ ‘ 𝑛 ) ∈ V )
53 2 fvexi ⊢ 𝑍 ∈ V
54 53 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑍 ∈ V )
55 2 49 eluzelz2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑛 ∈ ℤ )
56 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
57 55 uzidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
58 57 uzssd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑛 ) )
59 2 49 uzssd2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
60 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V )
61 18 52 54 55 56 58 59 60 climeqmpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
62 51 61 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
63 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝜑 )
64 nfv ⊢ Ⅎ 𝑚 𝜑
65 64 20 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
66 2 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ℤ )
68 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑀 ∈ ℤ )
69 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
70 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
71 65 67 68 56 2 69 70 limsupequzmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
72 63 49 71 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
73 62 72 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
74 73 climfvd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) )
75 74 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ) )
76 16 17 75 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
77 15 76 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) )
78 10 77 mpteq12dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
79 9 78 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
80 1 2 3 4 7 8 smflimsuplem3 ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↦ ( ⇝ ‘ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
81 79 80 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )