Metamath Proof Explorer

Theorem smflimsupmpt

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . A can contain m as a free variable, in other words it can be thought of as an indexed collection A ( m ) . B can be thought of as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsupmpt.p ⊢ Ⅎ 𝑚 𝜑
smflimsupmpt.x ⊢ Ⅎ 𝑥 𝜑
smflimsupmpt.n ⊢ Ⅎ 𝑛 𝜑
smflimsupmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsupmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsupmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsupmpt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
smflimsupmpt.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smflimsupmpt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ }
smflimsupmpt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
Assertion smflimsupmpt ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smflimsupmpt.p ⊢ Ⅎ 𝑚 𝜑
2 smflimsupmpt.x ⊢ Ⅎ 𝑥 𝜑
3 smflimsupmpt.n ⊢ Ⅎ 𝑛 𝜑
4 smflimsupmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 smflimsupmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 smflimsupmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
7 smflimsupmpt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
8 smflimsupmpt.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
9 smflimsupmpt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ }
10 smflimsupmpt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
11 10 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
12 9 a1i ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
14 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
15 1 14 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
16 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
17 5 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
18 17 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
20 8 elexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
21 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22 21 fvmpt2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
23 19 20 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
24 23 dmeqd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
25 nfv ⊢ Ⅎ 𝑥 𝑚 ∈ 𝑍
26 2 25 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑚 ∈ 𝑍 )
27 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
28 7 3expa ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
29 26 27 28 dmmptdf ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
30 24 29 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐴 = dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
31 16 18 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐴 = dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
32 15 31 iineq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
33 3 32 iuneq2df ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
35 13 34 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
36 35 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
37 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
38 37 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
40 nfv ⊢ Ⅎ 𝑛 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) )
41 nfcv ⊢ Ⅎ 𝑚 𝑥
42 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
43 41 42 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
44 1 14 43 nf3an ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
45 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
46 16 18 45 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
47 46 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
48 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
49 48 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
50 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
51 18 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
52 50 51 49 7 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐵 ∈ 𝑊 )
53 27 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
54 49 52 53 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
55 47 54 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = 𝐵 )
56 44 55 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
58 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑀 ∈ ℤ )
59 5 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
60 59 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ℤ )
61 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
62 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ 𝑍 ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
63 51 62 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
64 44 58 60 5 61 62 63 limsupequzmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
65 14 nfci ⊢ Ⅎ 𝑚 𝑍
66 nfcv ⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑛 )
67 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ 𝑍 )
68 60 uzidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
69 44 65 66 5 61 67 68 52 limsupequzmpt2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
70 57 64 69 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
71 70 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
72 3 40 71 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
74 39 73 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
76 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
77 75 76 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
78 36 77 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
79 78 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
80 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝜑 )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
82 33 eqcomd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
84 81 83 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
85 84 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
86 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
87 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
88 74 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
89 88 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
90 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
91 89 90 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
92 87 91 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
93 80 85 86 92 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
94 93 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) )
95 79 94 impbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
96 2 95 rabbida3 ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
97 12 96 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
98 9 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
99 98 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
100 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
101 99 100 syl ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
102 101 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
103 2 97 102 mpteq12da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
104 11 103 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
105 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
106 nfcv ⊢ Ⅎ 𝑥 𝑍
107 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
108 106 107 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
109 1 8 fmptd2f ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
110 eqid ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
111 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
112 105 108 4 5 6 109 110 111 smflimsup ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
113 104 112 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )