| Step | Hyp | Ref
| Expression |
| 1 | | smfliminf.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 2 | | smfliminf.z |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | | smfliminf.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 4 | | smfliminf.f |
. 2
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 5 | | smfliminf.d |
. . 3
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
| 6 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑖∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 7 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑛∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 8 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
| 9 | 8 | iineq1d 45095 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 10 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝐹‘𝑚) |
| 11 | 10 | nfdm 5962 |
. . . . . . . 8
⊢
Ⅎ𝑘dom
(𝐹‘𝑚) |
| 12 | | smfliminf.n |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝐹 |
| 13 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑘 |
| 14 | 12, 13 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝐹‘𝑘) |
| 15 | 14 | nfdm 5962 |
. . . . . . . 8
⊢
Ⅎ𝑚dom
(𝐹‘𝑘) |
| 16 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
| 17 | 16 | dmeqd 5916 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → dom (𝐹‘𝑚) = dom (𝐹‘𝑘)) |
| 18 | 11, 15, 17 | cbviin 5037 |
. . . . . . 7
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘)) |
| 20 | 9, 19 | eqtrd 2777 |
. . . . 5
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘)) |
| 21 | 6, 7, 20 | cbviun 5036 |
. . . 4
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 22 | 21 | rabeqi 3450 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
| 23 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥𝑍 |
| 24 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥(ℤ≥‘𝑖) |
| 25 | | smfliminf.x |
. . . . . . . 8
⊢
Ⅎ𝑥𝐹 |
| 26 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑘 |
| 27 | 25, 26 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐹‘𝑘) |
| 28 | 27 | nfdm 5962 |
. . . . . 6
⊢
Ⅎ𝑥dom
(𝐹‘𝑘) |
| 29 | 24, 28 | nfiin 5024 |
. . . . 5
⊢
Ⅎ𝑥∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 30 | 23, 29 | nfiun 5023 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 31 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
| 32 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑦(lim
inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ |
| 33 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥lim
inf |
| 34 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
| 35 | 27, 34 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑘)‘𝑦) |
| 36 | 23, 35 | nfmpt 5249 |
. . . . . 6
⊢
Ⅎ𝑥(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)) |
| 37 | 33, 36 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥(lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
| 38 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥ℝ |
| 39 | 37, 38 | nfel 2920 |
. . . 4
⊢
Ⅎ𝑥(lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ |
| 40 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑚 𝑥 = 𝑦 |
| 41 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
| 42 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
| 43 | 40, 42 | mpteq2da 5240 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
| 44 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝐹‘𝑚)‘𝑦) |
| 45 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑦 |
| 46 | 14, 45 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑘)‘𝑦) |
| 47 | 16 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑘)‘𝑦)) |
| 48 | 44, 46, 47 | cbvmpt 5253 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)) |
| 49 | 48 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
| 50 | 43, 49 | eqtrd 2777 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
| 51 | 50 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 𝑦 → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
| 52 | 51 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝑦 → ((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ ↔ (lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ)) |
| 53 | 30, 31, 32, 39, 52 | cbvrabw 3473 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ} |
| 54 | 5, 22, 53 | 3eqtri 2769 |
. 2
⊢ 𝐷 = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ} |
| 55 | | smfliminf.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 56 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
| 57 | 5, 56 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
| 58 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦𝐷 |
| 59 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦(lim
inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
| 60 | 57, 58, 59, 37, 51 | cbvmptf 5251 |
. . 3
⊢ (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
| 61 | 55, 60 | eqtri 2765 |
. 2
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
| 62 | 1, 2, 3, 4, 54, 61 | smfliminflem 46845 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |