Metamath Proof Explorer

Theorem smfliminfmpt

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) 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, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 smfliminfmpt.p ⊢ Ⅎ 𝑚 𝜑
2 smfliminfmpt.x ⊢ Ⅎ 𝑥 𝜑
3 smfliminfmpt.n ⊢ Ⅎ 𝑛 𝜑
4 smfliminfmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 smfliminfmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 smfliminfmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
7 smfliminfmpt.b ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
8 smfliminfmpt.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
9 smfliminfmpt.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ }
10 smfliminfmpt.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
11 10 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
12 9 a1i ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
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 inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
37 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
38 37 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
39 nfv ⊢ Ⅎ 𝑛 ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) )
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 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ 𝑍 )
51 50 17 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
52 49 51 48 7 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐵 ∈ 𝑉 )
53 27 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
54 48 52 53 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
55 46 54 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) = 𝐵 )
56 43 55 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
58 nfcv ⊢ Ⅎ 𝑚 𝑍
59 nfcv ⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑛 )
60 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
61 5 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
62 61 uzidd ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
63 62 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
64 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
65 43 58 59 5 60 50 63 64 liminfequzmpt2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
66 43 58 59 5 60 50 63 52 liminfequzmpt2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ 𝐵 ) ) )
67 57 65 66 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
68 67 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
69 3 39 68 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) )
71 38 70 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
72 71 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) )
73 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
74 72 73 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
75 36 74 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
76 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝜑 )
77 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) )
78 33 eqcomd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
80 77 79 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
81 80 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
82 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
83 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
84 71 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
85 84 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
86 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
87 85 86 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
88 83 87 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
89 76 81 82 88 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) )
90 75 89 impbida ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
91 2 90 rabbida3 ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
92 12 91 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
93 9 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
94 93 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } )
95 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
96 94 95 syl ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐴 )
97 96 84 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
98 2 92 97 mpteq12da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
99 11 98 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
100 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
101 nfcv ⊢ Ⅎ 𝑥 𝑍
102 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
103 101 102 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
104 1 8 fmptd2f ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
105 eqid ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
106 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
107 100 103 4 5 6 104 105 106 smfliminf ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( ( 𝑚 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
108 99 107 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )