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 2764 |
. . . . 5
⊢
Ⅎ𝑥𝑍 |
7 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥(ℤ≥‘𝑛) |
8 | | smfliminf.x |
. . . . . . . 8
⊢
Ⅎ𝑥𝐹 |
9 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑚 |
10 | 8, 9 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐹‘𝑚) |
11 | 10 | nfdm 5367 |
. . . . . 6
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) |
12 | 7, 11 | nfiin 4549 |
. . . . 5
⊢
Ⅎ𝑥∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
13 | 6, 12 | nfiun 4548 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
14 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥(ℤ≥‘𝑖) |
15 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑘 |
16 | 8, 15 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐹‘𝑘) |
17 | 16 | nfdm 5367 |
. . . . . 6
⊢
Ⅎ𝑥dom
(𝐹‘𝑘) |
18 | 14, 17 | nfiin 4549 |
. . . . 5
⊢
Ⅎ𝑥∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
19 | 6, 18 | nfiun 4548 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
20 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑖∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
21 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑛∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
22 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
23 | 22 | iineq1d 39267 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
24 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝐹‘𝑚) |
25 | 24 | nfdm 5367 |
. . . . . . . 8
⊢
Ⅎ𝑘dom
(𝐹‘𝑚) |
26 | | smfliminf.n |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝐹 |
27 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑘 |
28 | 26, 27 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝐹‘𝑘) |
29 | 28 | nfdm 5367 |
. . . . . . . 8
⊢
Ⅎ𝑚dom
(𝐹‘𝑘) |
30 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
31 | 30 | dmeqd 5326 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → dom (𝐹‘𝑚) = dom (𝐹‘𝑘)) |
32 | 25, 29, 31 | cbviin 4558 |
. . . . . . 7
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘)) |
34 | 23, 33 | eqtrd 2656 |
. . . . 5
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘)) |
35 | 20, 21, 34 | cbviun 4557 |
. . . 4
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
36 | 13, 19, 35 | rabeqif 3191 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
37 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑦∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) |
38 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑦(lim
inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ |
39 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥lim
inf |
40 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
41 | 16, 40 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑘)‘𝑦) |
42 | 6, 41 | nfmpt 4746 |
. . . . . 6
⊢
Ⅎ𝑥(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)) |
43 | 39, 42 | nffv 6198 |
. . . . 5
⊢
Ⅎ𝑥(lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
44 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑥ℝ |
45 | 43, 44 | nfel 2777 |
. . . 4
⊢
Ⅎ𝑥(lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ |
46 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑚 𝑥 = 𝑦 |
47 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
48 | 47 | adantr 481 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
49 | 46, 48 | mpteq2da 4743 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
50 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝐹‘𝑚)‘𝑦) |
51 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑦 |
52 | 28, 51 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑘)‘𝑦) |
53 | 30 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑘)‘𝑦)) |
54 | 50, 52, 53 | cbvmpt 4749 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)) |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
56 | 49, 55 | eqtrd 2656 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) |
57 | 56 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 𝑦 → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
58 | 57 | eleq1d 2686 |
. . . 4
⊢ (𝑥 = 𝑦 → ((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ ↔ (lim
inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ)) |
59 | 19, 37, 38, 45, 58 | cbvrab 3198 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ} |
60 | 5, 36, 59 | 3eqtri 2648 |
. 2
⊢ 𝐷 = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑘 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑘) ∣ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦))) ∈ ℝ} |
61 | | smfliminf.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
62 | | nfrab1 3122 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} |
63 | 5, 62 | nfcxfr 2762 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
64 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑦𝐷 |
65 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑦(lim
inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
66 | 63, 64, 65, 43, 57 | cbvmptf 4748 |
. . 3
⊢ (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
67 | 61, 66 | eqtri 2644 |
. 2
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (lim inf‘(𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑦)))) |
68 | 1, 2, 3, 4, 60, 67 | smfliminflem 41036 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |