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 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
39 nfv ⊢ Ⅎ 𝑛 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) )
40 nfcv ⊢ Ⅎ 𝑚 𝑥
41 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
42 40 41 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴
43 1 14 42 nf3an ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
44 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
45 16 18 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
46 45 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
47 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
48 47 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
49 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
50 18 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
51 49 50 48 7 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐵 ∈ 𝑊 )
52 27 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
53 48 51 52 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
54 46 53 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = 𝐵 )
55 43 54 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
56 55 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
57 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑀 ∈ ℤ )
58 5 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
59 58 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ℤ )
60 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
61 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ 𝑍 ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
62 50 61 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
63 43 57 59 5 60 61 62 limsupequzmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
64 14 nfci ⊢ Ⅎ 𝑚 𝑍
65 nfcv ⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑛 )
66 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ 𝑍 )
67 59 uzidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
68 43 64 65 5 60 66 67 51 limsupequzmpt2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
69 56 63 68 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
70 69 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
71 3 39 70 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
73 38 72 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
74 73 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
75 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
76 74 75 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
77 36 76 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
78 77 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
79 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝜑 )
80 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
81 33 eqcomd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
83 80 82 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
84 83 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
85 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
86 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
87 73 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
88 87 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
89 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
90 88 89 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
91 86 90 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
92 79 84 85 91 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
93 92 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) )
94 78 93 impbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
95 2 94 rabbida3 ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
96 12 95 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
97 9 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
98 97 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
99 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
100 98 99 syl ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
101 100 87 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
102 2 96 101 mpteq12da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
103 11 102 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
104 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
105 nfcv ⊢ Ⅎ 𝑥 𝑍
106 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
107 105 106 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
108 1 8 fmptd2f ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
109 eqid ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
110 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
111 104 107 4 5 6 108 109 110 smflimsup ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
112 103 111 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )