| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. 2
⊢
Ⅎ𝑎𝜑 |
| 2 | | smflim.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 3 | | smflim.d |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 4 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑍 |
| 5 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥(ℤ≥‘𝑛) |
| 6 | | smflim.x |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
| 7 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑚 |
| 8 | 6, 7 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐹‘𝑚) |
| 9 | 8 | nfdm 5962 |
. . . . . . . 8
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) |
| 10 | 5, 9 | nfiin 5024 |
. . . . . . 7
⊢
Ⅎ𝑥∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 11 | 4, 10 | nfiun 5023 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 12 | 11 | ssrab2f 45122 |
. . . . 5
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 13 | 3, 12 | eqsstri 4030 |
. . . 4
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐷 ⊆ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 15 | | uzssz 12899 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 16 | | smflim.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 17 | 16 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀)) |
| 18 | 17 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑀)) |
| 19 | 15, 18 | sselid 3981 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 20 | | uzid 12893 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
| 21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) |
| 22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑛)) |
| 23 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 24 | | smflim.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 25 | 24 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (SMblFn‘𝑆)) |
| 26 | | eqid 2737 |
. . . . . . 7
⊢ dom
(𝐹‘𝑛) = dom (𝐹‘𝑛) |
| 27 | 23, 25, 26 | smfdmss 46748 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ⊆ ∪ 𝑆) |
| 28 | | smflim.n |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝐹 |
| 29 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑛 |
| 30 | 28, 29 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝐹‘𝑛) |
| 31 | 30 | nfdm 5962 |
. . . . . . . 8
⊢
Ⅎ𝑚dom
(𝐹‘𝑛) |
| 32 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑚∪ 𝑆 |
| 33 | 31, 32 | nfss 3976 |
. . . . . . 7
⊢
Ⅎ𝑚dom (𝐹‘𝑛) ⊆ ∪ 𝑆 |
| 34 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 35 | 34 | dmeqd 5916 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → dom (𝐹‘𝑚) = dom (𝐹‘𝑛)) |
| 36 | 35 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (dom (𝐹‘𝑚) ⊆ ∪ 𝑆 ↔ dom (𝐹‘𝑛) ⊆ ∪ 𝑆)) |
| 37 | 33, 36 | rspce 3611 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘𝑛) ∧ dom (𝐹‘𝑛) ⊆ ∪ 𝑆) → ∃𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
| 38 | 22, 27, 37 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
| 39 | | iinss 5056 |
. . . . 5
⊢
(∃𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆 → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
| 40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
| 41 | 40 | iunssd 5050 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
| 42 | 14, 41 | sstrd 3994 |
. 2
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆) |
| 43 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑚𝜑 |
| 44 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑚𝑦 |
| 45 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
| 46 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚dom
⇝ |
| 47 | 45, 46 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ |
| 48 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚𝑍 |
| 49 | | nfii1 5029 |
. . . . . . . . 9
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 50 | 48, 49 | nfiun 5023 |
. . . . . . . 8
⊢
Ⅎ𝑚∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 51 | 47, 50 | nfrabw 3475 |
. . . . . . 7
⊢
Ⅎ𝑚{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 52 | 3, 51 | nfcxfr 2903 |
. . . . . 6
⊢
Ⅎ𝑚𝐷 |
| 53 | 44, 52 | nfel 2920 |
. . . . 5
⊢
Ⅎ𝑚 𝑦 ∈ 𝐷 |
| 54 | 43, 53 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑚(𝜑 ∧ 𝑦 ∈ 𝐷) |
| 55 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑤𝐹 |
| 56 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 57 | 24 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
| 58 | | eqid 2737 |
. . . . . 6
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
| 59 | 56, 57, 58 | smff 46747 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
| 60 | 59 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
| 61 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 62 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ |
| 63 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 |
| 64 | 8, 63 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑦) |
| 65 | 4, 64 | nfmpt 5249 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) |
| 66 | 65 | nfel1 2922 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ |
| 67 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
| 68 | 67 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
| 69 | 68 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ )) |
| 70 | 11, 61, 62, 66, 69 | cbvrabw 3473 |
. . . . . 6
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑦 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ } |
| 71 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑙dom
(𝐹‘𝑚) |
| 72 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚𝑙 |
| 73 | 28, 72 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(𝐹‘𝑙) |
| 74 | 73 | nfdm 5962 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚dom
(𝐹‘𝑙) |
| 75 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑙 → (𝐹‘𝑚) = (𝐹‘𝑙)) |
| 76 | 75 | dmeqd 5916 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑙 → dom (𝐹‘𝑚) = dom (𝐹‘𝑙)) |
| 77 | 71, 74, 76 | cbviin 5037 |
. . . . . . . . . . . 12
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) |
| 78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙)) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
| 80 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((𝑛 = 𝑖 ∧ 𝑙 ∈ (ℤ≥‘𝑖)) → dom (𝐹‘𝑙) = dom (𝐹‘𝑙)) |
| 81 | 79, 80 | iineq12dv 45111 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → ∩
𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) = ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
| 82 | 78, 81 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
| 83 | 82 | cbviunv 5040 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) |
| 84 | 83 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ 𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
| 85 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑙𝑍 |
| 86 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑦) |
| 87 | 73, 44 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑦) |
| 88 | 75 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑙 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑙)‘𝑦)) |
| 89 | 48, 85, 86, 87, 88 | cbvmptf 5251 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) |
| 90 | 89 | eleq1i 2832 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ ↔ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ ) |
| 91 | 84, 90 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ ) ↔ (𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∧ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ )) |
| 92 | 91 | rabbia2 3439 |
. . . . . 6
⊢ {𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ } = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } |
| 93 | 3, 70, 92 | 3eqtri 2769 |
. . . . 5
⊢ 𝐷 = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } |
| 94 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → ((𝐹‘𝑙)‘𝑦) = ((𝐹‘𝑙)‘𝑤)) |
| 95 | 94 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤))) |
| 96 | 95 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ ↔ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ )) |
| 97 | 96 | cbvrabv 3447 |
. . . . . 6
⊢ {𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ } |
| 98 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑚 → (𝐹‘𝑙) = (𝐹‘𝑚)) |
| 99 | 98 | dmeqd 5916 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → dom (𝐹‘𝑙) = dom (𝐹‘𝑚)) |
| 100 | 74, 71, 99 | cbviin 5037 |
. . . . . . . . . . 11
⊢ ∩ 𝑙 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
| 101 | 100 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑍 → ∩
𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 102 | 101 | iuneq2i 5013 |
. . . . . . . . 9
⊢ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
| 103 | 102 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ↔ 𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 104 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝑤 |
| 105 | 73, 104 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑤) |
| 106 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑤) |
| 107 | 98 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ((𝐹‘𝑙)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) |
| 108 | 85, 48, 105, 106, 107 | cbvmptf 5251 |
. . . . . . . . 9
⊢ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) |
| 109 | 108 | eleq1i 2832 |
. . . . . . . 8
⊢ ((𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ ) |
| 110 | 103, 109 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∧ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ ) ↔ (𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ )) |
| 111 | 110 | rabbia2 3439 |
. . . . . 6
⊢ {𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ } = {𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ } |
| 112 | 97, 111 | eqtri 2765 |
. . . . 5
⊢ {𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ } |
| 113 | 93, 112 | eqtri 2765 |
. . . 4
⊢ 𝐷 = {𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ } |
| 114 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
| 115 | 54, 28, 55, 16, 60, 113, 114 | fnlimfvre 45689 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) ∈ ℝ) |
| 116 | | smflim.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 117 | | nfrab1 3457 |
. . . . . 6
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 118 | 3, 117 | nfcxfr 2903 |
. . . . 5
⊢
Ⅎ𝑥𝐷 |
| 119 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦𝐷 |
| 120 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
| 121 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥
⇝ |
| 122 | 121, 65 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
| 123 | 68 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 𝑦 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
| 124 | 118, 119,
120, 122, 123 | cbvmptf 5251 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
| 125 | 116, 124 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
| 126 | 115, 125 | fmptd 7134 |
. 2
⊢ (𝜑 → 𝐺:𝐷⟶ℝ) |
| 127 | | smflim.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 128 | 127 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑀 ∈ ℤ) |
| 129 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑆 ∈ SAlg) |
| 130 | 24 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 131 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑙 |
| 132 | 6, 131 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐹‘𝑙) |
| 133 | 132, 63 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑙)‘𝑦) |
| 134 | 4, 133 | nfmpt 5249 |
. . . . . 6
⊢
Ⅎ𝑥(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) |
| 135 | 121, 134 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥(
⇝ ‘(𝑙 ∈
𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
| 136 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑥) |
| 137 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑥 |
| 138 | 73, 137 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑥) |
| 139 | 75 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑚 = 𝑙 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑙)‘𝑥)) |
| 140 | 48, 85, 136, 138, 139 | cbvmptf 5251 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥)) |
| 141 | 140 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥))) |
| 142 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍) → 𝑥 = 𝑦) |
| 143 | 142 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍) → ((𝐹‘𝑙)‘𝑥) = ((𝐹‘𝑙)‘𝑦)) |
| 144 | 143 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
| 145 | 141, 144 | eqtrd 2777 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
| 146 | 145 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 𝑦 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
| 147 | 118, 119,
120, 135, 146 | cbvmptf 5251 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
| 148 | 116, 147 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
| 149 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) |
| 150 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚
< |
| 151 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑎 + (1 / 𝑗)) |
| 152 | 87, 150, 151 | nfbr 5190 |
. . . . . . . 8
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) |
| 153 | 152, 74 | nfrabw 3475 |
. . . . . . 7
⊢
Ⅎ𝑚{𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} |
| 154 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑚𝑡 |
| 155 | 154, 74 | nfin 4224 |
. . . . . . 7
⊢
Ⅎ𝑚(𝑡 ∩ dom (𝐹‘𝑙)) |
| 156 | 153, 155 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑚{𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙)) |
| 157 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑚𝑆 |
| 158 | 156, 157 | nfrabw 3475 |
. . . . 5
⊢
Ⅎ𝑚{𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} |
| 159 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘{𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} |
| 160 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑙{𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
| 161 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑗{𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
| 162 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦dom
(𝐹‘𝑙) |
| 163 | 132 | nfdm 5962 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥dom
(𝐹‘𝑙) |
| 164 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
< |
| 165 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑎 + (1 / 𝑗)) |
| 166 | 133, 164,
165 | nfbr 5190 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) |
| 167 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) |
| 168 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑙)‘𝑦) = ((𝐹‘𝑙)‘𝑥)) |
| 169 | 168 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)))) |
| 170 | 162, 163,
166, 167, 169 | cbvrabw 3473 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} |
| 171 | 170 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))}) |
| 172 | | ineq1 4213 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑡 ∩ dom (𝐹‘𝑙)) = (𝑠 ∩ dom (𝐹‘𝑙))) |
| 173 | 171, 172 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ({𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙)) ↔ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙)))) |
| 174 | 173 | cbvrabv 3447 |
. . . . . . . 8
⊢ {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))} |
| 175 | 174 | a1i 11 |
. . . . . . 7
⊢ (𝑙 = 𝑚 → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))}) |
| 176 | 99 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → (𝑥 ∈ dom (𝐹‘𝑙) ↔ 𝑥 ∈ dom (𝐹‘𝑚))) |
| 177 | 98 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → ((𝐹‘𝑙)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) |
| 178 | 177 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → (((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)))) |
| 179 | 176, 178 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ((𝑥 ∈ dom (𝐹‘𝑙) ∧ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))) ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))))) |
| 180 | 179 | rabbidva2 3438 |
. . . . . . . . 9
⊢ (𝑙 = 𝑚 → {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))}) |
| 181 | 99 | ineq2d 4220 |
. . . . . . . . 9
⊢ (𝑙 = 𝑚 → (𝑠 ∩ dom (𝐹‘𝑙)) = (𝑠 ∩ dom (𝐹‘𝑚))) |
| 182 | 180, 181 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑙 = 𝑚 → ({𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
| 183 | 182 | rabbidv 3444 |
. . . . . . 7
⊢ (𝑙 = 𝑚 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 184 | 175, 183 | eqtrd 2777 |
. . . . . 6
⊢ (𝑙 = 𝑚 → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 185 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (1 / 𝑗) = (1 / 𝑘)) |
| 186 | 185 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑎 + (1 / 𝑗)) = (𝑎 + (1 / 𝑘))) |
| 187 | 186 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘)))) |
| 188 | 187 | rabbidv 3444 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))}) |
| 189 | 188 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
| 190 | 189 | rabbidv 3444 |
. . . . . 6
⊢ (𝑗 = 𝑘 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 191 | 184, 190 | sylan9eq 2797 |
. . . . 5
⊢ ((𝑙 = 𝑚 ∧ 𝑗 = 𝑘) → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 192 | 158, 159,
160, 161, 191 | cbvmpo 7527 |
. . . 4
⊢ (𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))}) = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 193 | 192 | eqcomi 2746 |
. . 3
⊢ (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) = (𝑙 ∈ 𝑍, 𝑗 ∈ ℕ ↦ {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))}) |
| 194 | 128, 16, 129, 130, 93, 148, 149, 193 | smflimlem6 46791 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ (𝐺‘𝑦) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷)) |
| 195 | 1, 2, 42, 126, 194 | issmfled 46772 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |