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