| Step | Hyp | Ref
| Expression |
| 1 | | smflimsuplem8.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))) |
| 3 | | smflimsuplem8.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 4 | | smflimsuplem8.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 5 | | smflimsuplem8.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 6 | | smflimsuplem8.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 7 | | smflimsuplem8.d |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
| 8 | | smflimsuplem8.e |
. . . . 5
⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) |
| 9 | | smflimsuplem8.h |
. . . . 5
⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) |
| 10 | 3, 4, 5, 6, 7, 8, 9 | smflimsuplem7 46841 |
. . . 4
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) |
| 11 | | rabidim1 3459 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 12 | | eliun 4995 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 13 | 11, 12 | sylib 218 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 14 | 13, 7 | eleq2s 2859 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 15 | 14 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 16 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐷) |
| 17 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑛(lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))) |
| 18 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 19 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(𝜑 ∧ 𝑥 ∈ 𝐷) |
| 20 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 |
| 21 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚𝑥 |
| 22 | | nfii1 5029 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 23 | 21, 22 | nfel 2920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 24 | 19, 20, 23 | nf3an 1901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 25 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑀 ∈ ℤ) |
| 26 | 25 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑀 ∈ ℤ) |
| 27 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑆 ∈ SAlg) |
| 28 | 27 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑆 ∈ SAlg) |
| 29 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 30 | 29 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 31 | | rabidim2 45107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |
| 32 | 31, 7 | eleq2s 2859 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐷 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |
| 33 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑦 → (𝐹‘𝑚) = (𝐹‘𝑦)) |
| 34 | 33 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑦)‘𝑥)) |
| 35 | 34 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑦 ∈ 𝑍 ↦ ((𝐹‘𝑦)‘𝑥)) |
| 36 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
| 37 | 36 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧)‘𝑥) = ((𝐹‘𝑦)‘𝑥)) |
| 38 | 37 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑍 ↦ ((𝐹‘𝑧)‘𝑥)) = (𝑦 ∈ 𝑍 ↦ ((𝐹‘𝑦)‘𝑥)) |
| 39 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤)) |
| 40 | 39 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧)‘𝑥) = ((𝐹‘𝑤)‘𝑥)) |
| 41 | 40 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑍 ↦ ((𝐹‘𝑧)‘𝑥)) = (𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥)) |
| 42 | 35, 38, 41 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥)) |
| 43 | 42 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢ (lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥))) |
| 44 | 43 | eleq1i 2832 |
. . . . . . . . . . . . . . 15
⊢ ((lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ ↔ (lim
sup‘(𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥))) ∈ ℝ) |
| 45 | 32, 44 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐷 → (lim sup‘(𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥))) ∈ ℝ) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim sup‘(𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥))) ∈ ℝ) |
| 47 | 46 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑤 ∈ 𝑍 ↦ ((𝐹‘𝑤)‘𝑥))) ∈ ℝ) |
| 48 | 47, 44 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |
| 49 | | simp2 1138 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍) |
| 50 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 51 | 18, 24, 26, 4, 28, 30, 8, 9, 48, 49, 50 | smflimsuplem5 46839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ (ℤ≥‘𝑛) ↦ ((𝐻‘𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 52 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ∈ V) |
| 53 | 4 | fvexi 6920 |
. . . . . . . . . . . 12
⊢ 𝑍 ∈ V |
| 54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑍 ∈ V) |
| 55 | 4, 49 | eluzelz2d 45424 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ ℤ) |
| 56 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
| 57 | 55 | uzidd 12894 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ (ℤ≥‘𝑛)) |
| 58 | 57 | uzssd 45419 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑛)) |
| 59 | 4, 49 | uzssd2 45428 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 60 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐻‘𝑘)‘𝑥) ∈ V) |
| 61 | 18, 52, 54, 55, 56, 58, 59, 60 | climeqmpt 45712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ((𝑘 ∈ (ℤ≥‘𝑛) ↦ ((𝐻‘𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))))) |
| 62 | 51, 61 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 63 | | simp1l 1198 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝜑) |
| 64 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚𝜑 |
| 65 | 64, 20 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 66 | 4 | eluzelz2 45414 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 67 | 66 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℤ) |
| 68 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ) |
| 69 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 70 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 71 | 65, 67, 68, 56, 4, 69, 70 | limsupequzmpt 45744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 72 | 63, 49, 71 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 73 | 62, 72 | breqtrd 5169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 74 | 73 | climfvd 45713 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)))) |
| 75 | 74 | 3exp 1120 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)))))) |
| 76 | 16, 17, 75 | rexlimd 3266 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))))) |
| 77 | 15, 76 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)))) |
| 78 | 10, 77 | mpteq12dva 5231 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))))) |
| 79 | 2, 78 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))))) |
| 80 | 3, 4, 5, 6, 8, 9 | smflimsuplem3 46837 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)))) ∈ (SMblFn‘𝑆)) |
| 81 | 79, 80 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |