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

Theorem smflimsuplem7 46781
Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
smflimsuplem7.m (𝜑𝑀 ∈ ℤ)
smflimsuplem7.z 𝑍 = (ℤ𝑀)
smflimsuplem7.s (𝜑𝑆 ∈ SAlg)
smflimsuplem7.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smflimsuplem7.d 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
smflimsuplem7.e 𝐸 = (𝑘𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
smflimsuplem7.h 𝐻 = (𝑘𝑍 ↦ (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
Assertion
Ref Expression
smflimsuplem7 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
Distinct variable groups:   𝑘,𝐸,𝑥   𝑘,𝐹,𝑚,𝑛,𝑥   𝑘,𝐻,𝑚,𝑛,𝑥   𝑚,𝑀   𝑘,𝑍,𝑚,𝑛,𝑥   𝜑,𝑘,𝑚,𝑛,𝑥
Allowed substitution hints:   𝐷(𝑥,𝑘,𝑚,𝑛)   𝑆(𝑥,𝑘,𝑚,𝑛)   𝐸(𝑚,𝑛)   𝑀(𝑥,𝑘,𝑛)

Proof of Theorem smflimsuplem7
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 smflimsuplem7.d . . 3 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
21a1i 11 . 2 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ})
3 simpl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝜑)
4 rabidim2 45041 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
54adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
6 rabidim1 3455 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
7 eliun 4999 . . . . . . . . . . 11 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
86, 7sylib 218 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
98adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
10 nfv 1911 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
11 nfv 1911 . . . . . . . . . . . . . . . . . . 19 𝑚𝜑
12 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑚lim sup
13 nfmpt1 5255 . . . . . . . . . . . . . . . . . . . . 21 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
1412, 13nffv 6916 . . . . . . . . . . . . . . . . . . . 20 𝑚(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
15 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑚
1614, 15nfel 2917 . . . . . . . . . . . . . . . . . . 19 𝑚(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ
1711, 16nfan 1896 . . . . . . . . . . . . . . . . . 18 𝑚(𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
18 nfv 1911 . . . . . . . . . . . . . . . . . 18 𝑚 𝑛𝑍
19 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑚𝑥
20 nfii1 5033 . . . . . . . . . . . . . . . . . . 19 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2119, 20nfel 2917 . . . . . . . . . . . . . . . . . 18 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2217, 18, 21nf3an 1898 . . . . . . . . . . . . . . . . 17 𝑚((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
23 nfv 1911 . . . . . . . . . . . . . . . . 17 𝑚 𝑘 ∈ (ℤ𝑛)
2422, 23nfan 1896 . . . . . . . . . . . . . . . 16 𝑚(((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛))
25 simpl1l 1223 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝜑)
26 smflimsuplem7.m . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑀 ∈ ℤ)
28 smflimsuplem7.z . . . . . . . . . . . . . . . 16 𝑍 = (ℤ𝑀)
29 smflimsuplem7.s . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ SAlg)
3025, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑆 ∈ SAlg)
31 smflimsuplem7.f . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
3225, 31syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
33 smflimsuplem7.e . . . . . . . . . . . . . . . 16 𝐸 = (𝑘𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
34 smflimsuplem7.h . . . . . . . . . . . . . . . 16 𝐻 = (𝑘𝑍 ↦ (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
3528uztrn2 12894 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍𝑘 ∈ (ℤ𝑛)) → 𝑘𝑍)
36353ad2antl2 1185 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘𝑍)
37 simpl1r 1224 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
38 uzss 12898 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ𝑛) → (ℤ𝑘) ⊆ (ℤ𝑛))
39 iinss1 5011 . . . . . . . . . . . . . . . . . . . 20 ((ℤ𝑘) ⊆ (ℤ𝑛) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ𝑛) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4140adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
42 simpl 482 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
4341, 42sseldd 3995 . . . . . . . . . . . . . . . . 17 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
44433ad2antl3 1186 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4524, 27, 28, 30, 32, 33, 34, 36, 37, 44smflimsuplem2 46776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 ∈ dom (𝐻𝑘))
4645ralrimiva 3143 . . . . . . . . . . . . . 14 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘))
47 vex 3481 . . . . . . . . . . . . . . 15 𝑥 ∈ V
48 eliin 5000 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘)))
4947, 48ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘))
5046, 49sylibr 234 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
51503exp 1118 . . . . . . . . . . . 12 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))))
5210, 51reximdai 3258 . . . . . . . . . . 11 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)))
5352imp 406 . . . . . . . . . 10 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
54 eliun 4999 . . . . . . . . . 10 (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
5553, 54sylibr 234 . . . . . . . . 9 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
563, 5, 9, 55syl21anc 838 . . . . . . . 8 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
577biimpi 216 . . . . . . . . . . 11 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
586, 57syl 17 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
5958adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
60 nfv 1911 . . . . . . . . . . 11 𝑛𝜑
61 nfcv 2902 . . . . . . . . . . . 12 𝑛𝑥
62 nfv 1911 . . . . . . . . . . . . 13 𝑛(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ
63 nfiu1 5031 . . . . . . . . . . . . 13 𝑛 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
6462, 63nfrabw 3472 . . . . . . . . . . . 12 𝑛{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
6561, 64nfel 2917 . . . . . . . . . . 11 𝑛 𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
6660, 65nfan 1896 . . . . . . . . . 10 𝑛(𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ})
67 nfv 1911 . . . . . . . . . 10 𝑛(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝
68 nfv 1911 . . . . . . . . . . . . 13 𝑘((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
69 simp1l 1196 . . . . . . . . . . . . . 14 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝜑)
7069, 26syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑀 ∈ ℤ)
7169, 29syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑆 ∈ SAlg)
7269, 31syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
73 simp1r 1197 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
74 simp2 1136 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛𝑍)
75 simp3 1137 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
7668, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75smflimsuplem6 46780 . . . . . . . . . . . 12 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
77763exp 1118 . . . . . . . . . . 11 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )))
785, 77syldan 591 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )))
7966, 67, 78rexlimd 3263 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
8059, 79mpd 15 . . . . . . . 8 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
8156, 80jca 511 . . . . . . 7 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
82 rabid 3454 . . . . . . 7 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
8381, 82sylibr 234 . . . . . 6 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
8483ex 412 . . . . 5 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
85 ssrab2 4089 . . . . . . . . . 10 {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
8685a1i 11 . . . . . . . . 9 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
8728eluzelz2 45352 . . . . . . . . . . . . . . 15 (𝑛𝑍𝑛 ∈ ℤ)
8887uzidd 12891 . . . . . . . . . . . . . 14 (𝑛𝑍𝑛 ∈ (ℤ𝑛))
8988adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → 𝑛 ∈ (ℤ𝑛))
90 nfv 1911 . . . . . . . . . . . . . . . . 17 𝑥(𝜑𝑛𝑍)
91 xrltso 13179 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
9291a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐸𝑛)) → < Or ℝ*)
9392supexd 9490 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐸𝑛)) → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ V)
94 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ))
9590, 93, 94fnmptd 6709 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸𝑛))
96 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → (𝐸𝑘) = (𝐸𝑛))
97 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑛 → (ℤ𝑘) = (ℤ𝑛))
9897mpteq1d 5242 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑛 → (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))
9998rneqd 5951 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))
10099supeq1d 9483 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ))
10196, 100mpteq12dv 5238 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
102 fvex 6919 . . . . . . . . . . . . . . . . . . . 20 (𝐸𝑛) ∈ V
103102mptex 7242 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) ∈ V
104101, 34, 103fvmpt 7015 . . . . . . . . . . . . . . . . . 18 (𝑛𝑍 → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
105104adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
106105fneq1d 6661 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → ((𝐻𝑛) Fn (𝐸𝑛) ↔ (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸𝑛)))
10795, 106mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐻𝑛) Fn (𝐸𝑛))
108107fndmd 6673 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → dom (𝐻𝑛) = (𝐸𝑛))
10997iineq1d 45029 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) = 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
110109eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ↔ 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)))
111100eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ))
112110, 111anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ) ↔ (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ)))
113112rabbidva2 3434 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
114 id 22 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛𝑍)
115 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑦))
116115mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
117116rneqd 5951 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
118117supeq1d 9483 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ))
119118eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ))
120119cbvrabv 3443 . . . . . . . . . . . . . . . . . 18 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑦 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ}
12188ne0d 4347 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑍 → (ℤ𝑛) ≠ ∅)
122 fvex 6919 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ∈ V
123122dmex 7931 . . . . . . . . . . . . . . . . . . . . 21 dom (𝐹𝑚) ∈ V
124123rgenw 3062 . . . . . . . . . . . . . . . . . . . 20 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V
125124a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑍 → ∀𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
126121, 125iinexd 45072 . . . . . . . . . . . . . . . . . 18 (𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
127120, 126rabexd 5345 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ∈ V)
12833, 113, 114, 127fvmptd3 7038 . . . . . . . . . . . . . . . 16 (𝑛𝑍 → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
129128adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
130 ssrab2 4089 . . . . . . . . . . . . . . . 16 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
131130a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
132129, 131eqsstrd 4033 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
133108, 132eqsstrd 4033 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
134 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (𝐻𝑘) = (𝐻𝑛))
135134dmeqd 5918 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → dom (𝐻𝑘) = dom (𝐻𝑛))
136135sseq1d 4026 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)))
137136rspcev 3621 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑛) ∧ dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
13889, 133, 137syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → ∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
139 iinss 5060 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
140138, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
141140ralrimiva 3143 . . . . . . . . . 10 (𝜑 → ∀𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
142 ss2iun 5014 . . . . . . . . . 10 (∀𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
143141, 142syl 17 . . . . . . . . 9 (𝜑 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14486, 143sstrd 4005 . . . . . . . 8 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14582simplbi 497 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
14654biimpi 216 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
147145, 146syl 17 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
148147adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
149 nfiu1 5031 . . . . . . . . . . . . . 14 𝑛 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
15067, 149nfrabw 3472 . . . . . . . . . . . . 13 𝑛{𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
15161, 150nfel 2917 . . . . . . . . . . . 12 𝑛 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
15260, 151nfan 1896 . . . . . . . . . . 11 𝑛(𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
15382simprbi 496 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
154 nfv 1911 . . . . . . . . . . . . . . . 16 𝑘𝜑
155 nfmpt1 5255 . . . . . . . . . . . . . . . . 17 𝑘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))
156 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑘dom ⇝
157155, 156nfel 2917 . . . . . . . . . . . . . . . 16 𝑘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝
158154, 157nfan 1896 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
159 nfv 1911 . . . . . . . . . . . . . . 15 𝑘 𝑛𝑍
160 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑘𝑥
161 nfii1 5033 . . . . . . . . . . . . . . . 16 𝑘 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
162160, 161nfel 2917 . . . . . . . . . . . . . . 15 𝑘 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
163158, 159, 162nf3an 1898 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
16426adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝑀 ∈ ℤ)
1651643adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑀 ∈ ℤ)
1661653adant1r 1176 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑀 ∈ ℤ)
16729adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
1681673adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑆 ∈ SAlg)
1691683adant1r 1176 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑆 ∈ SAlg)
17031adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
1711703adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
1721713adant1r 1176 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
173 simp2 1136 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑛𝑍)
174 simp3 1137 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
175 simp1r 1197 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
176163, 166, 28, 169, 172, 33, 34, 173, 174, 175smflimsuplem4 46778 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
1771763exp 1118 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)))
178153, 177sylan2 593 . . . . . . . . . . 11 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛𝑍 → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)))
179152, 62, 178rexlimd 3263 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
180148, 179mpd 15 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
181180ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
182144, 181jca 511 . . . . . . 7 (𝜑 → ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
183 nfrab1 3453 . . . . . . . 8 𝑥{𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
184 nfcv 2902 . . . . . . . 8 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
185183, 184ssrabf 45053 . . . . . . 7 ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
186182, 185sylibr 234 . . . . . 6 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ})
187186sseld 3993 . . . . 5 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}))
18884, 187impbid 212 . . . 4 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
189188alrimiv 1924 . . 3 (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
190 nfrab1 3453 . . . 4 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
191190, 183cleqf 2931 . . 3 ({𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
192189, 191sylibr 234 . 2 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
1932, 192eqtrd 2774 1 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wcel 2105  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  wss 3962   ciun 4995   ciin 4996  cmpt 5230   Or wor 5595  dom cdm 5688  ran crn 5689   Fn wfn 6557  wf 6558  cfv 6562  supcsup 9477  cr 11151  *cxr 11291   < clt 11292  cz 12610  cuz 12875  lim supclsp 15502  cli 15516  SAlgcsalg 46263  SMblFncsmblfn 46650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-rp 13032  df-ioo 13387  df-ico 13389  df-fz 13544  df-fl 13828  df-ceil 13829  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-smblfn 46651
This theorem is referenced by:  smflimsuplem8  46782
  Copyright terms: Public domain W3C validator