| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smflimsuplem7.d | . . 3
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) | 
| 3 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝜑) | 
| 4 |  | rabidim2 45107 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 5 | 4 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 6 |  | rabidim1 3459 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 7 |  | eliun 4995 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 8 | 6, 7 | sylib 218 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 9 | 8 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 10 |  | nfv 1914 | . . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 11 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝜑 | 
| 12 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑚lim
sup | 
| 13 |  | nfmpt1 5250 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) | 
| 14 | 12, 13 | nffv 6916 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚(lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) | 
| 15 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚ℝ | 
| 16 | 14, 15 | nfel 2920 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚(lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ | 
| 17 | 11, 16 | nfan 1899 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 18 |  | nfv 1914 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 | 
| 19 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝑥 | 
| 20 |  | nfii1 5029 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) | 
| 21 | 19, 20 | nfel 2920 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) | 
| 22 | 17, 18, 21 | nf3an 1901 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 23 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚 𝑘 ∈
(ℤ≥‘𝑛) | 
| 24 | 22, 23 | nfan 1899 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) | 
| 25 |  | simpl1l 1225 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝜑) | 
| 26 |  | smflimsuplem7.m | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑀 ∈ ℤ) | 
| 28 |  | smflimsuplem7.z | . . . . . . . . . . . . . . . 16
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 29 |  | smflimsuplem7.s | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 30 | 25, 29 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑆 ∈ SAlg) | 
| 31 |  | smflimsuplem7.f | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 32 | 25, 31 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 33 |  | smflimsuplem7.e | . . . . . . . . . . . . . . . 16
⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 34 |  | smflimsuplem7.h | . . . . . . . . . . . . . . . 16
⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 35 | 28 | uztrn2 12897 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ 𝑍) | 
| 36 | 35 | 3ad2antl2 1187 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ 𝑍) | 
| 37 |  | simpl1r 1226 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 38 |  | uzss 12901 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (ℤ≥‘𝑘) ⊆
(ℤ≥‘𝑛)) | 
| 39 |  | iinss1 5007 | . . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ≥‘𝑘) ⊆ (ℤ≥‘𝑛) → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚)) | 
| 40 | 38, 39 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚)) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚)) | 
| 42 |  | simpl 482 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 43 | 41, 42 | sseldd 3984 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚)) | 
| 44 | 43 | 3ad2antl3 1188 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚)) | 
| 45 | 24, 27, 28, 30, 32, 33, 34, 36, 37, 44 | smflimsuplem2 46836 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘)) | 
| 46 | 45 | ralrimiva 3146 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘)) | 
| 47 |  | vex 3484 | . . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V | 
| 48 |  | eliin 4996 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))) | 
| 49 | 47, 48 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘)) | 
| 50 | 46, 49 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 51 | 50 | 3exp 1120 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)))) | 
| 52 | 10, 51 | reximdai 3261 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘))) | 
| 53 | 52 | imp 406 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 54 |  | eliun 4995 | . . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 55 | 53, 54 | sylibr 234 | . . . . . . . . 9
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 56 | 3, 5, 9, 55 | syl21anc 838 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 57 | 7 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 58 | 6, 57 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 59 | 58 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 60 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑛𝜑 | 
| 61 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑛𝑥 | 
| 62 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛(lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ | 
| 63 |  | nfiu1 5027 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) | 
| 64 | 62, 63 | nfrabw 3475 | . . . . . . . . . . . 12
⊢
Ⅎ𝑛{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} | 
| 65 | 61, 64 | nfel 2920 | . . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} | 
| 66 | 60, 65 | nfan 1899 | . . . . . . . . . 10
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) | 
| 67 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑛(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ | 
| 68 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 69 |  | simp1l 1198 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝜑) | 
| 70 | 69, 26 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑀 ∈ ℤ) | 
| 71 | 69, 29 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑆 ∈ SAlg) | 
| 72 | 69, 31 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 73 |  | simp1r 1199 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 74 |  | simp2 1138 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍) | 
| 75 |  | simp3 1139 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 76 | 68, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75 | smflimsuplem6 46840 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) | 
| 77 | 76 | 3exp 1120 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))) | 
| 78 | 5, 77 | syldan 591 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))) | 
| 79 | 66, 67, 78 | rexlimd 3266 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )) | 
| 80 | 59, 79 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) | 
| 81 | 56, 80 | jca 511 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )) | 
| 82 |  | rabid 3458 | . . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )) | 
| 83 | 81, 82 | sylibr 234 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) | 
| 84 | 83 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })) | 
| 85 |  | ssrab2 4080 | . . . . . . . . . 10
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) | 
| 86 | 85 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 87 | 28 | eluzelz2 45414 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) | 
| 88 | 87 | uzidd 12894 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) | 
| 89 | 88 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑛)) | 
| 90 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍) | 
| 91 |  | xrltso 13183 | . . . . . . . . . . . . . . . . . . 19
⊢  < Or
ℝ* | 
| 92 | 91 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or
ℝ*) | 
| 93 | 92 | supexd 9493 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
V) | 
| 94 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) | 
| 95 | 90, 93, 94 | fnmptd 6709 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸‘𝑛)) | 
| 96 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛)) | 
| 97 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑛 → (ℤ≥‘𝑘) =
(ℤ≥‘𝑛)) | 
| 98 | 97 | mpteq1d 5237 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) | 
| 99 | 98 | rneqd 5949 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥))) | 
| 100 | 99 | supeq1d 9486 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
)) | 
| 101 | 96, 100 | mpteq12dv 5233 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 102 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸‘𝑛) ∈ V | 
| 103 | 102 | mptex 7243 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) ∈
V | 
| 104 | 101, 34, 103 | fvmpt 7016 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 105 | 104 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, <
))) | 
| 106 | 105 | fneq1d 6661 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )) Fn (𝐸‘𝑛))) | 
| 107 | 95, 106 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛)) | 
| 108 | 107 | fndmd 6673 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛)) | 
| 109 | 97 | iineq1d 45095 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 110 | 109 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚))) | 
| 111 | 100 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ ↔ sup(ran (𝑚
∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ)) | 
| 112 | 110, 111 | anbi12d 632 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → ((𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ) ↔ (𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ))) | 
| 113 | 112 | rabbidva2 3438 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑥 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 114 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) | 
| 115 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) | 
| 116 | 115 | mpteq2dv 5244 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦))) | 
| 117 | 116 | rneqd 5949 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦))) | 
| 118 | 117 | supeq1d 9486 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) = sup(ran
(𝑚 ∈
(ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, <
)) | 
| 119 | 118 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ ↔ sup(ran (𝑚
∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ)) | 
| 120 | 119 | cbvrabv 3447 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} = {𝑦 ∈
∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ*, < ) ∈
ℝ} | 
| 121 | 88 | ne0d 4342 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅) | 
| 122 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹‘𝑚) ∈ V | 
| 123 | 122 | dmex 7931 | . . . . . . . . . . . . . . . . . . . . 21
⊢ dom
(𝐹‘𝑚) ∈ V | 
| 124 | 123 | rgenw 3065 | . . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V | 
| 125 | 124 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) | 
| 126 | 121, 125 | iinexd 45138 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) | 
| 127 | 120, 126 | rabexd 5340 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ∈ V) | 
| 128 | 33, 113, 114, 127 | fvmptd3 7039 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 129 | 128 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ}) | 
| 130 |  | ssrab2 4080 | . . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ⊆ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) | 
| 131 | 130 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈
ℝ} ⊆ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 132 | 129, 131 | eqsstrd 4018 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 133 | 108, 132 | eqsstrd 4018 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 134 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛)) | 
| 135 | 134 | dmeqd 5916 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛)) | 
| 136 | 135 | sseq1d 4015 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚))) | 
| 137 | 136 | rspcev 3622 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 138 | 89, 133, 137 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 139 |  | iinss 5056 | . . . . . . . . . . . 12
⊢
(∃𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 140 | 138, 139 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 141 | 140 | ralrimiva 3146 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 142 |  | ss2iun 5010 | . . . . . . . . . 10
⊢
(∀𝑛 ∈
𝑍 ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) → ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 143 | 141, 142 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 144 | 86, 143 | sstrd 3994 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) | 
| 145 | 82 | simplbi 497 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 146 | 54 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 147 | 145, 146 | syl 17 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 148 | 147 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 149 |  | nfiu1 5027 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) | 
| 150 | 67, 149 | nfrabw 3475 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } | 
| 151 | 61, 150 | nfel 2920 | . . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } | 
| 152 | 60, 151 | nfan 1899 | . . . . . . . . . . 11
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) | 
| 153 | 82 | simprbi 496 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) | 
| 154 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝜑 | 
| 155 |  | nfmpt1 5250 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) | 
| 156 |  | nfcv 2905 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘dom
⇝ | 
| 157 | 155, 156 | nfel 2920 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ | 
| 158 | 154, 157 | nfan 1899 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) | 
| 159 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘 𝑛 ∈ 𝑍 | 
| 160 |  | nfcv 2905 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝑥 | 
| 161 |  | nfii1 5029 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) | 
| 162 | 160, 161 | nfel 2920 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘 𝑥 ∈ ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) | 
| 163 | 158, 159,
162 | nf3an 1901 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑘((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 164 | 26 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ) | 
| 165 | 164 | 3adant3 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ) | 
| 166 | 165 | 3adant1r 1178 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ) | 
| 167 | 29 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) | 
| 168 | 167 | 3adant3 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg) | 
| 169 | 168 | 3adant1r 1178 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg) | 
| 170 | 31 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 171 | 170 | 3adant3 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 172 | 171 | 3adant1r 1178 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 173 |  | simp2 1138 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑛 ∈ 𝑍) | 
| 174 |  | simp3 1139 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) | 
| 175 |  | simp1r 1199 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) | 
| 176 | 163, 166,
28, 169, 172, 33, 34, 173, 174, 175 | smflimsuplem4 46838 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 177 | 176 | 3exp 1120 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))) | 
| 178 | 153, 177 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))) | 
| 179 | 152, 62, 178 | rexlimd 3266 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)) | 
| 180 | 148, 179 | mpd 15 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 181 | 180 | ralrimiva 3146 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) | 
| 182 | 144, 181 | jca 511 | . . . . . . 7
⊢ (𝜑 → ({𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)) | 
| 183 |  | nfrab1 3457 | . . . . . . . 8
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } | 
| 184 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) | 
| 185 | 183, 184 | ssrabf 45119 | . . . . . . 7
⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)) | 
| 186 | 182, 185 | sylibr 234 | . . . . . 6
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) | 
| 187 | 186 | sseld 3982 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})) | 
| 188 | 84, 187 | impbid 212 | . . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })) | 
| 189 | 188 | alrimiv 1927 | . . 3
⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })) | 
| 190 |  | nfrab1 3457 | . . . 4
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} | 
| 191 | 190, 183 | cleqf 2934 | . . 3
⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })) | 
| 192 | 189, 191 | sylibr 234 | . 2
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) | 
| 193 | 2, 192 | eqtrd 2777 | 1
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) |