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