Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimsupmpt Structured version   Visualization version   GIF version

Theorem smflimsupmpt 46208
Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
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
Ref Expression
smflimsupmpt (𝜑𝐺 ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝐴,𝑛,𝑥   𝐵,𝑛   𝑚,𝑀   𝑆,𝑚   𝑚,𝑍,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑚,𝑛)   𝐴(𝑚)   𝐵(𝑥,𝑚)   𝐷(𝑥,𝑚,𝑛)   𝑆(𝑥,𝑛)   𝐺(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑛)   𝑊(𝑥,𝑚,𝑛)

Proof of Theorem smflimsupmpt
StepHypRef Expression
1 smflimsupmpt.g . . . 4 𝐺 = (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍𝐵)))
21a1i 11 . . 3 (𝜑𝐺 = (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍𝐵))))
3 smflimsupmpt.x . . . 4 𝑥𝜑
4 smflimsupmpt.d . . . . . 6 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ}
54a1i 11 . . . . 5 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ})
6 simpr 484 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
7 smflimsupmpt.n . . . . . . . . . . . . 13 𝑛𝜑
8 smflimsupmpt.p . . . . . . . . . . . . . . 15 𝑚𝜑
9 nfv 1910 . . . . . . . . . . . . . . 15 𝑚 𝑛𝑍
108, 9nfan 1895 . . . . . . . . . . . . . 14 𝑚(𝜑𝑛𝑍)
11 simpll 766 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
12 smflimsupmpt.z . . . . . . . . . . . . . . . . 17 𝑍 = (ℤ𝑀)
1312uztrn2 12866 . . . . . . . . . . . . . . . 16 ((𝑛𝑍𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
1413adantll 713 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
15 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍) → 𝑚𝑍)
16 smflimsupmpt.f . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
1716elexd 3491 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍) → (𝑥𝐴𝐵) ∈ V)
18 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑍 ↦ (𝑥𝐴𝐵)) = (𝑚𝑍 ↦ (𝑥𝐴𝐵))
1918fvmpt2 7011 . . . . . . . . . . . . . . . . . 18 ((𝑚𝑍 ∧ (𝑥𝐴𝐵) ∈ V) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
2015, 17, 19syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚𝑍) → ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = (𝑥𝐴𝐵))
2120dmeqd 5903 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑍) → dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = dom (𝑥𝐴𝐵))
22 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑥 𝑚𝑍
233, 22nfan 1895 . . . . . . . . . . . . . . . . 17 𝑥(𝜑𝑚𝑍)
24 eqid 2728 . . . . . . . . . . . . . . . . 17 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
25 smflimsupmpt.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚𝑍𝑥𝐴) → 𝐵𝑊)
26253expa 1116 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚𝑍) ∧ 𝑥𝐴) → 𝐵𝑊)
2723, 24, 26dmmptdf 44588 . . . . . . . . . . . . . . . 16 ((𝜑𝑚𝑍) → dom (𝑥𝐴𝐵) = 𝐴)
2821, 27eqtr2d 2769 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑍) → 𝐴 = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
2911, 14, 28syl2anc 583 . . . . . . . . . . . . . 14 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐴 = dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
3010, 29iineq2d 5015 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
317, 30iuneq2df 44401 . . . . . . . . . . . 12 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
3231adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
336, 32eleqtrd 2831 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
3433adantrr 716 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
35 eliun 4996 . . . . . . . . . . . . . 14 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
3635biimpi 215 . . . . . . . . . . . . 13 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
3736adantl 481 . . . . . . . . . . . 12 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
38 nfv 1910 . . . . . . . . . . . . . 14 𝑛(lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵))
39 nfcv 2899 . . . . . . . . . . . . . . . . . . . 20 𝑚𝑥
40 nfii1 5027 . . . . . . . . . . . . . . . . . . . 20 𝑚 𝑚 ∈ (ℤ𝑛)𝐴
4139, 40nfel 2913 . . . . . . . . . . . . . . . . . . 19 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)𝐴
428, 9, 41nf3an 1897 . . . . . . . . . . . . . . . . . 18 𝑚(𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴)
4320fveq1d 6894 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = ((𝑥𝐴𝐵)‘𝑥))
4411, 14, 43syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = ((𝑥𝐴𝐵)‘𝑥))
45443adantl3 1166 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = ((𝑥𝐴𝐵)‘𝑥))
46 eliinid 44468 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 𝑚 ∈ (ℤ𝑛)𝐴𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
47463ad2antl3 1185 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑥𝐴)
48 simpl1 1189 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝜑)
49143adantl3 1166 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
5048, 49, 47, 25syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐵𝑊)
5124fvmpt2 7011 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
5247, 50, 51syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
5345, 52eqtrd 2768 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) = 𝐵)
5442, 53mpteq2da 5241 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (𝑚 ∈ (ℤ𝑛) ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ 𝐵))
5554fveq2d 6896 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ 𝐵)))
56 smflimsupmpt.m . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℤ)
57563ad2ant1 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑀 ∈ ℤ)
5812eluzelz2 44776 . . . . . . . . . . . . . . . . . 18 (𝑛𝑍𝑛 ∈ ℤ)
59583ad2ant2 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ ℤ)
60 eqid 2728 . . . . . . . . . . . . . . . . 17 (ℤ𝑛) = (ℤ𝑛)
61 fvexd 6907 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚𝑍) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) ∈ V)
6249, 61syldan 590 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) ∧ 𝑚 ∈ (ℤ𝑛)) → (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥) ∈ V)
6342, 57, 59, 12, 60, 61, 62limsupequzmpt 45108 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
649nfci 2882 . . . . . . . . . . . . . . . . 17 𝑚𝑍
65 nfcv 2899 . . . . . . . . . . . . . . . . 17 𝑚(ℤ𝑛)
66 simp2 1135 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛𝑍)
6759uzidd 12863 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → 𝑛 ∈ (ℤ𝑛))
6842, 64, 65, 12, 60, 66, 67, 50limsupequzmpt2 45097 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚𝑍𝐵)) = (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ 𝐵)))
6955, 63, 683eqtr4d 2778 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵)))
70693exp 1117 . . . . . . . . . . . . . 14 (𝜑 → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵)))))
717, 38, 70rexlimd 3259 . . . . . . . . . . . . 13 (𝜑 → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵))))
7271adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)𝐴 → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵))))
7337, 72mpd 15 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵)))
7473adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍𝐵)))
75 simprr 772 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)) → (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)
7674, 75eqeltrd 2829 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)
7734, 76jca 511 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ))
7877ex 412 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)))
79 simpl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝜑)
80 simpr 484 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚))
8131eqcomd 2734 . . . . . . . . . . . 12 (𝜑 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8281adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)) → 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8380, 82eleqtrd 2831 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8483adantrr 716 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
85 simprr 772 . . . . . . . . 9 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)
86 simp2 1135 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
8773eqcomd 2734 . . . . . . . . . . . 12 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴) → (lim sup‘(𝑚𝑍𝐵)) = (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
88873adant3 1130 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚𝑍𝐵)) = (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
89 simp3 1136 . . . . . . . . . . 11 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)
9088, 89eqeltrd 2829 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)
9186, 90jca 511 . . . . . . . . 9 ((𝜑𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ))
9279, 84, 85, 91syl3anc 1369 . . . . . . . 8 ((𝜑 ∧ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ))
9392ex 412 . . . . . . 7 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ)))
9478, 93impbid 211 . . . . . 6 (𝜑 → ((𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∧ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ) ↔ (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∧ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ)))
953, 94rabbida3 44492 . . . . 5 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ} = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ})
965, 95eqtrd 2768 . . . 4 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ})
974eleq2i 2821 . . . . . . 7 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ})
9897biimpi 215 . . . . . 6 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ})
99 rabidim1 3449 . . . . . 6 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴 ∣ (lim sup‘(𝑚𝑍𝐵)) ∈ ℝ} → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
10098, 99syl 17 . . . . 5 (𝑥𝐷𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)𝐴)
101100, 87sylan2 592 . . . 4 ((𝜑𝑥𝐷) → (lim sup‘(𝑚𝑍𝐵)) = (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
1023, 96, 101mpteq12da 5228 . . 3 (𝜑 → (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍𝐵))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
1032, 102eqtrd 2768 . 2 (𝜑𝐺 = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))))
104 nfmpt1 5251 . . 3 𝑚(𝑚𝑍 ↦ (𝑥𝐴𝐵))
105 nfcv 2899 . . . 4 𝑥𝑍
106 nfmpt1 5251 . . . 4 𝑥(𝑥𝐴𝐵)
107105, 106nfmpt 5250 . . 3 𝑥(𝑚𝑍 ↦ (𝑥𝐴𝐵))
108 smflimsupmpt.s . . 3 (𝜑𝑆 ∈ SAlg)
1098, 16fmptd2f 44600 . . 3 (𝜑 → (𝑚𝑍 ↦ (𝑥𝐴𝐵)):𝑍⟶(SMblFn‘𝑆))
110 eqid 2728 . . 3 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ}
111 eqid 2728 . . 3 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))))
112104, 107, 56, 12, 108, 109, 110, 111smflimsup 46207 . 2 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom ((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚𝑍 ↦ (((𝑚𝑍 ↦ (𝑥𝐴𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
113103, 112eqeltrd 2829 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wnf 1778  wcel 2099  wrex 3066  {crab 3428  Vcvv 3470   ciun 4992   ciin 4993  cmpt 5226  dom cdm 5673  cfv 6543  cr 11132  cz 12583  cuz 12847  lim supclsp 15441  SAlgcsalg 45687  SMblFncsmblfn 46074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cc 10453  ax-ac2 10481  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7866  df-1st 7988  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-1o 8481  df-oadd 8485  df-omul 8486  df-er 8719  df-map 8841  df-pm 8842  df-en 8959  df-dom 8960  df-sdom 8961  df-fin 8962  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-acn 9960  df-ac 10134  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-z 12584  df-uz 12848  df-q 12958  df-rp 13002  df-ioo 13355  df-ioc 13356  df-ico 13357  df-fz 13512  df-fl 13784  df-ceil 13785  df-seq 13994  df-exp 14054  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-rest 17398  df-topgen 17419  df-top 22790  df-bases 22843  df-salg 45688  df-salgen 45692  df-smblfn 46075
This theorem is referenced by:  smfliminflem  46209
  Copyright terms: Public domain W3C validator