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

Theorem smflimsuplem7 41353
 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 472 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝜑)
4 rabidim2 39598 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
54adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
6 rabidim1 3147 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
7 eliun 4556 . . . . . . . . . . 11 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
86, 7sylib 208 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
98adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
10 nfv 1883 . . . . . . . . . . . 12 𝑛(𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
11 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑚𝜑
12 nfcv 2793 . . . . . . . . . . . . . . . . . . . . 21 𝑚lim sup
13 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . 21 𝑚(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
1412, 13nffv 6236 . . . . . . . . . . . . . . . . . . . 20 𝑚(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))
15 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑚
1614, 15nfel 2806 . . . . . . . . . . . . . . . . . . 19 𝑚(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ
1711, 16nfan 1868 . . . . . . . . . . . . . . . . . 18 𝑚(𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
18 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑚 𝑛𝑍
19 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑚𝑥
20 nfii1 4583 . . . . . . . . . . . . . . . . . . 19 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2119, 20nfel 2806 . . . . . . . . . . . . . . . . . 18 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2217, 18, 21nf3an 1871 . . . . . . . . . . . . . . . . 17 𝑚((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
23 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑚 𝑘 ∈ (ℤ𝑛)
2422, 23nfan 1868 . . . . . . . . . . . . . . . 16 𝑚(((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛))
25 simpl1l 1132 . . . . . . . . . . . . . . . . 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 11743 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍𝑘 ∈ (ℤ𝑛)) → 𝑘𝑍)
36353ad2antl2 1244 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘𝑍)
37 simpl1r 1133 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
38 uzss 11746 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ𝑛) → (ℤ𝑘) ⊆ (ℤ𝑛))
39 iinss1 4565 . . . . . . . . . . . . . . . . . . . 20 ((ℤ𝑘) ⊆ (ℤ𝑛) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ𝑛) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4140adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
42 simpl 472 . . . . . . . . . . . . . . . . . 18 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
4341, 42sseldd 3637 . . . . . . . . . . . . . . . . 17 ((𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
44433ad2antl3 1245 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚))
4524, 27, 28, 30, 32, 33, 34, 36, 37, 44smflimsuplem2 41348 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑥 ∈ dom (𝐻𝑘))
4645ralrimiva 2995 . . . . . . . . . . . . . 14 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘))
47 vex 3234 . . . . . . . . . . . . . . 15 𝑥 ∈ V
48 eliin 4557 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘)))
4947, 48ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∀𝑘 ∈ (ℤ𝑛)𝑥 ∈ dom (𝐻𝑘))
5046, 49sylibr 224 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
51503exp 1283 . . . . . . . . . . . 12 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))))
5210, 51reximdai 3041 . . . . . . . . . . 11 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)))
5352imp 444 . . . . . . . . . 10 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
54 eliun 4556 . . . . . . . . . 10 (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ↔ ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
5553, 54sylibr 224 . . . . . . . . 9 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
563, 5, 9, 55syl21anc 1365 . . . . . . . 8 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
577biimpi 206 . . . . . . . . . . 11 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
586, 57syl 17 . . . . . . . . . 10 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
5958adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
60 nfv 1883 . . . . . . . . . . 11 𝑛𝜑
61 nfcv 2793 . . . . . . . . . . . 12 𝑛𝑥
62 nfv 1883 . . . . . . . . . . . . 13 𝑛(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ
63 nfiu1 4582 . . . . . . . . . . . . 13 𝑛 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
6462, 63nfrab 3153 . . . . . . . . . . . 12 𝑛{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
6561, 64nfel 2806 . . . . . . . . . . 11 𝑛 𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
6660, 65nfan 1868 . . . . . . . . . 10 𝑛(𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ})
67 nfv 1883 . . . . . . . . . 10 𝑛(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝
68 nfv 1883 . . . . . . . . . . . . 13 𝑘((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
69 simp1l 1105 . . . . . . . . . . . . . 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 1106 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
74 simp2 1082 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛𝑍)
75 simp3 1083 . . . . . . . . . . . . 13 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
7668, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75smflimsuplem6 41352 . . . . . . . . . . . 12 (((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
77763exp 1283 . . . . . . . . . . 11 ((𝜑 ∧ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )))
785, 77syldan 486 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )))
7966, 67, 78rexlimd 3055 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
8059, 79mpd 15 . . . . . . . 8 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
8156, 80jca 553 . . . . . . 7 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
82 rabid 3145 . . . . . . 7 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ))
8381, 82sylibr 224 . . . . . 6 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
8483ex 449 . . . . 5 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
85 ssrab2 3720 . . . . . . . . . 10 {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
8685a1i 11 . . . . . . . . 9 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
8728eluzelz2 39940 . . . . . . . . . . . . . . 15 (𝑛𝑍𝑛 ∈ ℤ)
8887uzidd 39944 . . . . . . . . . . . . . 14 (𝑛𝑍𝑛 ∈ (ℤ𝑛))
8988adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → 𝑛 ∈ (ℤ𝑛))
90 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑥(𝜑𝑛𝑍)
91 xrltso 12012 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
9291a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐸𝑛)) → < Or ℝ*)
9392supexd 8400 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐸𝑛)) → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ V)
94 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ))
9590, 93, 94fnmptd 39748 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸𝑛))
96 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → (𝐸𝑘) = (𝐸𝑛))
97 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑛 → (ℤ𝑘) = (ℤ𝑛))
9897mpteq1d 4771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑛 → (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))
9998rneqd 5385 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))
10099supeq1d 8393 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ))
10196, 100mpteq12dv 4766 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
102 fvex 6239 . . . . . . . . . . . . . . . . . . . 20 (𝐸𝑛) ∈ V
103102mptex 6527 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) ∈ V
104101, 34, 103fvmpt 6321 . . . . . . . . . . . . . . . . . 18 (𝑛𝑍 → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
105104adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
106105fneq1d 6019 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → ((𝐻𝑛) Fn (𝐸𝑛) ↔ (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸𝑛)))
10795, 106mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐻𝑛) Fn (𝐸𝑛))
108107fndmd 39755 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → dom (𝐻𝑛) = (𝐸𝑛))
10997iineq1d 39581 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) = 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
110109eleq2d 2716 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ↔ 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)))
111100eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ))
112110, 111anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ) ↔ (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ)))
113112rabbidva2 3217 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
114 id 22 . . . . . . . . . . . . . . . . 17 (𝑛𝑍𝑛𝑍)
115 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑦))
116115mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
117116rneqd 5385 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
118117supeq1d 8393 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ))
119118eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ))
120119cbvrabv 3230 . . . . . . . . . . . . . . . . . 18 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑦 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ}
121 ne0i 3954 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑛) → (ℤ𝑛) ≠ ∅)
12288, 121syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑍 → (ℤ𝑛) ≠ ∅)
123 fvex 6239 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ∈ V
124123dmex 7141 . . . . . . . . . . . . . . . . . . . . 21 dom (𝐹𝑚) ∈ V
125124rgenw 2953 . . . . . . . . . . . . . . . . . . . 20 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V
126125a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑍 → ∀𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
127122, 126iinexd 39632 . . . . . . . . . . . . . . . . . 18 (𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
128120, 127rabexd 4846 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ∈ V)
12933, 113, 114, 128fvmptd3 39761 . . . . . . . . . . . . . . . 16 (𝑛𝑍 → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
130129adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
131 ssrab2 3720 . . . . . . . . . . . . . . . 16 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
132131a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
133130, 132eqsstrd 3672 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
134108, 133eqsstrd 3672 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
135 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (𝐻𝑘) = (𝐻𝑛))
136135dmeqd 5358 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → dom (𝐻𝑘) = dom (𝐻𝑛))
137136sseq1d 3665 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)))
138137rspcev 3340 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑛) ∧ dom (𝐻𝑛) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
13989, 134, 138syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → ∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
140 iinss 4603 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
141139, 140syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
142141ralrimiva 2995 . . . . . . . . . 10 (𝜑 → ∀𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
143 ss2iun 4568 . . . . . . . . . 10 (∀𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
144142, 143syl 17 . . . . . . . . 9 (𝜑 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14586, 144sstrd 3646 . . . . . . . 8 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
14682simplbi 475 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
14754biimpi 206 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
148146, 147syl 17 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
149148adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
150 nfiu1 4582 . . . . . . . . . . . . . 14 𝑛 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
15167, 150nfrab 3153 . . . . . . . . . . . . 13 𝑛{𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
15261, 151nfel 2806 . . . . . . . . . . . 12 𝑛 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
15360, 152nfan 1868 . . . . . . . . . . 11 𝑛(𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
15482simprbi 479 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
155 nfv 1883 . . . . . . . . . . . . . . . 16 𝑘𝜑
156 nfmpt1 4780 . . . . . . . . . . . . . . . . 17 𝑘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))
157 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑘dom ⇝
158156, 157nfel 2806 . . . . . . . . . . . . . . . 16 𝑘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝
159155, 158nfan 1868 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
160 nfv 1883 . . . . . . . . . . . . . . 15 𝑘 𝑛𝑍
161 nfcv 2793 . . . . . . . . . . . . . . . 16 𝑘𝑥
162 nfii1 4583 . . . . . . . . . . . . . . . 16 𝑘 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
163161, 162nfel 2806 . . . . . . . . . . . . . . 15 𝑘 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)
164159, 160, 163nf3an 1871 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
16526adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝑀 ∈ ℤ)
1661653adant3 1101 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑀 ∈ ℤ)
1671663adant1r 1359 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑀 ∈ ℤ)
16829adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
1691683adant3 1101 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑆 ∈ SAlg)
1701693adant1r 1359 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑆 ∈ SAlg)
17131adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
1721713adant3 1101 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
1731723adant1r 1359 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
174 simp2 1082 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑛𝑍)
175 simp3 1083 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘))
176 simp1r 1106 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ )
177164, 167, 28, 170, 173, 33, 34, 174, 175, 176smflimsuplem4 41350 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛𝑍𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
1781773exp 1283 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛𝑍 → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)))
179154, 178sylan2 490 . . . . . . . . . . 11 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛𝑍 → (𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)))
180153, 62, 179rexlimd 3055 . . . . . . . . . 10 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛𝑍 𝑥 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
181149, 180mpd 15 . . . . . . . . 9 ((𝜑𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
182181ralrimiva 2995 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
183145, 182jca 553 . . . . . . 7 (𝜑 → ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
184 nfrab1 3152 . . . . . . . 8 𝑥{𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }
185 nfcv 2793 . . . . . . . 8 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
186184, 185ssrabf 39612 . . . . . . 7 ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ ∀𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ))
187183, 186sylibr 224 . . . . . 6 (𝜑 → {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ})
188187sseld 3635 . . . . 5 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}))
18984, 188impbid 202 . . . 4 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
190189alrimiv 1895 . . 3 (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
191 nfrab1 3152 . . . 4 𝑥{𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
192191, 184dfcleqf 39569 . . 3 ({𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ }))
193190, 192sylibr 224 . 2 (𝜑 → {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
1942, 193eqtrd 2685 1 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  ∪ ciun 4552  ∩ ciin 4553   ↦ cmpt 4762   Or wor 5063  dom cdm 5143  ran crn 5144   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  supcsup 8387  ℝcr 9973  ℝ*cxr 10111   < clt 10112  ℤcz 11415  ℤ≥cuz 11725  lim supclsp 14245   ⇝ cli 14259  SAlgcsalg 40846  SMblFncsmblfn 41230 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-ioo 12217  df-ico 12219  df-fz 12365  df-fl 12633  df-ceil 12634  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-smblfn 41231 This theorem is referenced by:  smflimsuplem8  41354
 Copyright terms: Public domain W3C validator