Proof of Theorem smflimsupmpt
| Step | Hyp | Ref
| Expression |
| 1 | | smflimsupmpt.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
| 3 | | smflimsupmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 4 | | smflimsupmpt.d |
. . . . . 6
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
| 6 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 7 | | smflimsupmpt.n |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝜑 |
| 8 | | smflimsupmpt.p |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚𝜑 |
| 9 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 |
| 10 | 8, 9 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 11 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 12 | | smflimsupmpt.z |
. . . . . . . . . . . . . . . . 17
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 13 | 12 | uztrn2 12897 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 14 | 13 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 15 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 16 | | smflimsupmpt.f |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 17 | 16 | elexd 3504 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 18 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 19 | 18 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ 𝑍 ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 20 | 15, 17, 19 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 21 | 20 | dmeqd 5916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 22 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥 𝑚 ∈ 𝑍 |
| 23 | 3, 22 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ 𝑍) |
| 24 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 25 | | smflimsupmpt.b |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 26 | 25 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 27 | 23, 24, 26 | dmmptdf 45229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
| 28 | 21, 27 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 29 | 11, 14, 28 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐴 = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 30 | 10, 29 | iineq2d 5015 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 31 | 7, 30 | iuneq2df 45052 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 33 | 6, 32 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 34 | 33 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 35 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 36 | 35 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 38 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) |
| 39 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚𝑥 |
| 40 | | nfii1 5029 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 |
| 41 | 39, 40 | nfel 2920 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 |
| 42 | 8, 9, 41 | nf3an 1901 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 43 | 20 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 44 | 11, 14, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 45 | 44 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 46 | | eliinid 45116 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
| 47 | 46 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
| 48 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 49 | 14 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 50 | 48, 49, 47, 25 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ 𝑊) |
| 51 | 24 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 52 | 47, 50, 51 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 53 | 45, 52 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = 𝐵) |
| 54 | 42, 53 | mpteq2da 5240 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵)) |
| 55 | 54 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵))) |
| 56 | | smflimsupmpt.m |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 57 | 56 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑀 ∈ ℤ) |
| 58 | 12 | eluzelz2 45414 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 59 | 58 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ ℤ) |
| 60 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
| 61 | | fvexd 6921 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ 𝑍) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) ∈ V) |
| 62 | 49, 61 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) ∈ V) |
| 63 | 42, 57, 59, 12, 60, 61, 62 | limsupequzmpt 45744 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 64 | 9 | nfci 2893 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚𝑍 |
| 65 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(ℤ≥‘𝑛) |
| 66 | | simp2 1138 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ 𝑍) |
| 67 | 59 | uzidd 12894 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ (ℤ≥‘𝑛)) |
| 68 | 42, 64, 65, 12, 60, 66, 67, 50 | limsupequzmpt2 45733 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim sup‘(𝑚 ∈ (ℤ≥‘𝑛) ↦ 𝐵))) |
| 69 | 55, 63, 68 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 70 | 69 | 3exp 1120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))))) |
| 71 | 7, 38, 70 | rexlimd 3266 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
| 73 | 37, 72 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 74 | 73 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 75 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
| 76 | 74, 75 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
| 77 | 34, 76 | jca 511 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) |
| 78 | 77 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ))) |
| 79 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝜑) |
| 80 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 81 | 31 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 83 | 80, 82 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 84 | 83 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 85 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
| 86 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 87 | 73 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 88 | 87 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 89 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) |
| 90 | 88, 89 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (lim
sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) |
| 91 | 86, 90 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) |
| 92 | 79, 84, 85, 91 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ)) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)) |
| 93 | 92 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ))) |
| 94 | 78, 93 | impbid 212 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ) ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ))) |
| 95 | 3, 94 | rabbida3 45140 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ}) |
| 96 | 5, 95 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ}) |
| 97 | 4 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
| 98 | 97 | biimpi 216 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}) |
| 99 | | rabidim1 3459 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ} → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 100 | 98, 99 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 101 | 100, 87 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 102 | 3, 96, 101 | mpteq12da 5227 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
| 103 | 2, 102 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
| 104 | | nfmpt1 5250 |
. . 3
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 105 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑥𝑍 |
| 106 | | nfmpt1 5250 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 107 | 105, 106 | nfmpt 5249 |
. . 3
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 108 | | smflimsupmpt.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 109 | 8, 16 | fmptd2f 45240 |
. . 3
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)):𝑍⟶(SMblFn‘𝑆)) |
| 110 | | eqid 2737 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} |
| 111 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 112 | 104, 107,
56, 12, 108, 109, 110, 111 | smflimsup 46843 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim
sup‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆)) |
| 113 | 103, 112 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |