Step | Hyp | Ref
| Expression |
1 | | nfv 1922 |
. 2
⊢
Ⅎ𝑎𝜑 |
2 | | smflim.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
3 | | smflim.d |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
4 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥𝑍 |
5 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑥(ℤ≥‘𝑛) |
6 | | smflim.x |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
7 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑚 |
8 | 6, 7 | nffv 6727 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐹‘𝑚) |
9 | 8 | nfdm 5820 |
. . . . . . . 8
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) |
10 | 5, 9 | nfiin 4935 |
. . . . . . 7
⊢
Ⅎ𝑥∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
11 | 4, 10 | nfiun 4934 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
12 | 11 | ssrab2f 42339 |
. . . . 5
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
13 | 3, 12 | eqsstri 3935 |
. . . 4
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐷 ⊆ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
15 | | uzssz 12459 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
16 | | smflim.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
17 | 16 | eleq2i 2829 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀)) |
18 | 17 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑀)) |
19 | 15, 18 | sseldi 3899 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
20 | | uzid 12453 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑛)) |
22 | 21 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ≥‘𝑛)) |
23 | 2 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) |
24 | | smflim.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
25 | 24 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (SMblFn‘𝑆)) |
26 | | eqid 2737 |
. . . . . . 7
⊢ dom
(𝐹‘𝑛) = dom (𝐹‘𝑛) |
27 | 23, 25, 26 | smfdmss 43941 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ⊆ ∪ 𝑆) |
28 | | smflim.n |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝐹 |
29 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑛 |
30 | 28, 29 | nffv 6727 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝐹‘𝑛) |
31 | 30 | nfdm 5820 |
. . . . . . . 8
⊢
Ⅎ𝑚dom
(𝐹‘𝑛) |
32 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑚∪ 𝑆 |
33 | 31, 32 | nfss 3892 |
. . . . . . 7
⊢
Ⅎ𝑚dom (𝐹‘𝑛) ⊆ ∪ 𝑆 |
34 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
35 | 34 | dmeqd 5774 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → dom (𝐹‘𝑚) = dom (𝐹‘𝑛)) |
36 | 35 | sseq1d 3932 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (dom (𝐹‘𝑚) ⊆ ∪ 𝑆 ↔ dom (𝐹‘𝑛) ⊆ ∪ 𝑆)) |
37 | 33, 36 | rspce 3526 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘𝑛) ∧ dom (𝐹‘𝑛) ⊆ ∪ 𝑆) → ∃𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
38 | 22, 27, 37 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
39 | | iinss 4965 |
. . . . 5
⊢
(∃𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆 → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
41 | 40 | iunssd 4959 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∪ 𝑆) |
42 | 14, 41 | sstrd 3911 |
. 2
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆) |
43 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑚𝜑 |
44 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑚𝑦 |
45 | | nfmpt1 5153 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
46 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑚dom
⇝ |
47 | 45, 46 | nfel 2918 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ |
48 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑚𝑍 |
49 | | nfii1 4939 |
. . . . . . . . 9
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
50 | 48, 49 | nfiun 4934 |
. . . . . . . 8
⊢
Ⅎ𝑚∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
51 | 47, 50 | nfrabw 3297 |
. . . . . . 7
⊢
Ⅎ𝑚{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
52 | 3, 51 | nfcxfr 2902 |
. . . . . 6
⊢
Ⅎ𝑚𝐷 |
53 | 44, 52 | nfel 2918 |
. . . . 5
⊢
Ⅎ𝑚 𝑦 ∈ 𝐷 |
54 | 43, 53 | nfan 1907 |
. . . 4
⊢
Ⅎ𝑚(𝜑 ∧ 𝑦 ∈ 𝐷) |
55 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑤𝐹 |
56 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
57 | 24 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
58 | | eqid 2737 |
. . . . . 6
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
59 | 56, 57, 58 | smff 43940 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
60 | 59 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
61 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑦∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
62 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ |
63 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑦 |
64 | 8, 63 | nffv 6727 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑦) |
65 | 4, 64 | nfmpt 5152 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) |
66 | 65 | nfel1 2920 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ |
67 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦)) |
68 | 67 | mpteq2dv 5151 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
69 | 68 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ )) |
70 | 11, 61, 62, 66, 69 | cbvrabw 3400 |
. . . . . 6
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑦 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ } |
71 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑙dom
(𝐹‘𝑚) |
72 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚𝑙 |
73 | 28, 72 | nffv 6727 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(𝐹‘𝑙) |
74 | 73 | nfdm 5820 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑚dom
(𝐹‘𝑙) |
75 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑙 → (𝐹‘𝑚) = (𝐹‘𝑙)) |
76 | 75 | dmeqd 5774 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑙 → dom (𝐹‘𝑚) = dom (𝐹‘𝑙)) |
77 | 71, 74, 76 | cbviin 4946 |
. . . . . . . . . . . 12
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙)) |
79 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
80 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((𝑛 = 𝑖 ∧ 𝑙 ∈ (ℤ≥‘𝑖)) → dom (𝐹‘𝑙) = dom (𝐹‘𝑙)) |
81 | 79, 80 | iineq12dv 42329 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → ∩
𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) = ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
82 | 78, 81 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
83 | 82 | cbviunv 4949 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) |
84 | 83 | eleq2i 2829 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ 𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙)) |
85 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑙𝑍 |
86 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑦) |
87 | 73, 44 | nffv 6727 |
. . . . . . . . . 10
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑦) |
88 | 75 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑙 → ((𝐹‘𝑚)‘𝑦) = ((𝐹‘𝑙)‘𝑦)) |
89 | 48, 85, 86, 87, 88 | cbvmptf 5154 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) |
90 | 89 | eleq1i 2828 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ ↔ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ ) |
91 | 84, 90 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ ) ↔ (𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∧ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ )) |
92 | 91 | rabbia2 3387 |
. . . . . 6
⊢ {𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)) ∈ dom ⇝ } = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } |
93 | 3, 70, 92 | 3eqtri 2769 |
. . . . 5
⊢ 𝐷 = {𝑦 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } |
94 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → ((𝐹‘𝑙)‘𝑦) = ((𝐹‘𝑙)‘𝑤)) |
95 | 94 | mpteq2dv 5151 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤))) |
96 | 95 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ ↔ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ )) |
97 | 96 | cbvrabv 3402 |
. . . . . 6
⊢ {𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) ∈ dom ⇝ } = {𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∣ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ } |
98 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑚 → (𝐹‘𝑙) = (𝐹‘𝑚)) |
99 | 98 | dmeqd 5774 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → dom (𝐹‘𝑙) = dom (𝐹‘𝑚)) |
100 | 74, 71, 99 | cbviin 4946 |
. . . . . . . . . . 11
⊢ ∩ 𝑙 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
101 | 100 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑍 → ∩
𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
102 | 101 | iuneq2i 4925 |
. . . . . . . . 9
⊢ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
103 | 102 | eleq2i 2829 |
. . . . . . . 8
⊢ (𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ↔ 𝑤 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
104 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝑤 |
105 | 73, 104 | nffv 6727 |
. . . . . . . . . 10
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑤) |
106 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑤) |
107 | 98 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ((𝐹‘𝑙)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) |
108 | 85, 48, 105, 106, 107 | cbvmptf 5154 |
. . . . . . . . 9
⊢ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) |
109 | 108 | eleq1i 2828 |
. . . . . . . 8
⊢ ((𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ ) |
110 | 103, 109 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑙) ∧ (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑤)) ∈ dom ⇝ ) ↔ (𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ∧ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) ∈ dom ⇝ )) |
111 | 110 | rabbia2 3387 |
. . . . . 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 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
115 | 54, 28, 55, 16, 60, 113, 114 | fnlimfvre 42890 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) ∈ ℝ) |
116 | | smflim.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
117 | | nfrab1 3296 |
. . . . . 6
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
118 | 3, 117 | nfcxfr 2902 |
. . . . 5
⊢
Ⅎ𝑥𝐷 |
119 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑦𝐷 |
120 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑦(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
121 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥
⇝ |
122 | 121, 65 | nffv 6727 |
. . . . 5
⊢
Ⅎ𝑥(
⇝ ‘(𝑚 ∈
𝑍 ↦ ((𝐹‘𝑚)‘𝑦))) |
123 | 68 | fveq2d 6721 |
. . . . 5
⊢ (𝑥 = 𝑦 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
124 | 118, 119,
120, 122, 123 | cbvmptf 5154 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
125 | 116, 124 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑦)))) |
126 | 115, 125 | fmptd 6931 |
. 2
⊢ (𝜑 → 𝐺:𝐷⟶ℝ) |
127 | | smflim.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
128 | 127 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑀 ∈ ℤ) |
129 | 2 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑆 ∈ SAlg) |
130 | 24 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
131 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑙 |
132 | 6, 131 | nffv 6727 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐹‘𝑙) |
133 | 132, 63 | nffv 6727 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑙)‘𝑦) |
134 | 4, 133 | nfmpt 5152 |
. . . . . 6
⊢
Ⅎ𝑥(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)) |
135 | 121, 134 | nffv 6727 |
. . . . 5
⊢
Ⅎ𝑥(
⇝ ‘(𝑙 ∈
𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
136 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑙((𝐹‘𝑚)‘𝑥) |
137 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑚𝑥 |
138 | 73, 137 | nffv 6727 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑥) |
139 | 75 | fveq1d 6719 |
. . . . . . . . 9
⊢ (𝑚 = 𝑙 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑙)‘𝑥)) |
140 | 48, 85, 136, 138, 139 | cbvmptf 5154 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥)) |
141 | 140 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥))) |
142 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍) → 𝑥 = 𝑦) |
143 | 142 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍) → ((𝐹‘𝑙)‘𝑥) = ((𝐹‘𝑙)‘𝑦)) |
144 | 143 | mpteq2dva 5150 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
145 | 141, 144 | eqtrd 2777 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦))) |
146 | 145 | fveq2d 6721 |
. . . . 5
⊢ (𝑥 = 𝑦 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
147 | 118, 119,
120, 135, 146 | cbvmptf 5154 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
148 | 116, 147 | eqtri 2765 |
. . 3
⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ ( ⇝ ‘(𝑙 ∈ 𝑍 ↦ ((𝐹‘𝑙)‘𝑦)))) |
149 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) |
150 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑚
< |
151 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑎 + (1 / 𝑗)) |
152 | 87, 150, 151 | nfbr 5100 |
. . . . . . . 8
⊢
Ⅎ𝑚((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) |
153 | 152, 74 | nfrabw 3297 |
. . . . . . 7
⊢
Ⅎ𝑚{𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} |
154 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑚𝑡 |
155 | 154, 74 | nfin 4131 |
. . . . . . 7
⊢
Ⅎ𝑚(𝑡 ∩ dom (𝐹‘𝑙)) |
156 | 153, 155 | nfeq 2917 |
. . . . . 6
⊢
Ⅎ𝑚{𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙)) |
157 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑚𝑆 |
158 | 156, 157 | nfrabw 3297 |
. . . . 5
⊢
Ⅎ𝑚{𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} |
159 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑘{𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} |
160 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑙{𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
161 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑗{𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
162 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦dom
(𝐹‘𝑙) |
163 | 132 | nfdm 5820 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥dom
(𝐹‘𝑙) |
164 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
< |
165 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑎 + (1 / 𝑗)) |
166 | 133, 164,
165 | nfbr 5100 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) |
167 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) |
168 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑙)‘𝑦) = ((𝐹‘𝑙)‘𝑥)) |
169 | 168 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)))) |
170 | 162, 163,
166, 167, 169 | cbvrabw 3400 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} |
171 | 170 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))}) |
172 | | ineq1 4120 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑡 ∩ dom (𝐹‘𝑙)) = (𝑠 ∩ dom (𝐹‘𝑙))) |
173 | 171, 172 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ({𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙)) ↔ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙)))) |
174 | 173 | cbvrabv 3402 |
. . . . . . . 8
⊢ {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))} |
175 | 174 | a1i 11 |
. . . . . . 7
⊢ (𝑙 = 𝑚 → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))}) |
176 | 99 | eleq2d 2823 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → (𝑥 ∈ dom (𝐹‘𝑙) ↔ 𝑥 ∈ dom (𝐹‘𝑚))) |
177 | 98 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → ((𝐹‘𝑙)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) |
178 | 177 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → (((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)))) |
179 | 176, 178 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ((𝑥 ∈ dom (𝐹‘𝑙) ∧ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))) ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))))) |
180 | 179 | rabbidva2 3386 |
. . . . . . . . 9
⊢ (𝑙 = 𝑚 → {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))}) |
181 | 99 | ineq2d 4127 |
. . . . . . . . 9
⊢ (𝑙 = 𝑚 → (𝑠 ∩ dom (𝐹‘𝑙)) = (𝑠 ∩ dom (𝐹‘𝑚))) |
182 | 180, 181 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑙 = 𝑚 → ({𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
183 | 182 | rabbidv 3390 |
. . . . . . 7
⊢ (𝑙 = 𝑚 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
184 | 175, 183 | eqtrd 2777 |
. . . . . 6
⊢ (𝑙 = 𝑚 → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
185 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (1 / 𝑗) = (1 / 𝑘)) |
186 | 185 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑎 + (1 / 𝑗)) = (𝑎 + (1 / 𝑘))) |
187 | 186 | breq2d 5065 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗)) ↔ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘)))) |
188 | 187 | rabbidv 3390 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))}) |
189 | 188 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
190 | 189 | rabbidv 3390 |
. . . . . 6
⊢ (𝑗 = 𝑘 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
191 | 184, 190 | sylan9eq 2798 |
. . . . 5
⊢ ((𝑙 = 𝑚 ∧ 𝑗 = 𝑘) → {𝑡 ∈ 𝑆 ∣ {𝑦 ∈ dom (𝐹‘𝑙) ∣ ((𝐹‘𝑙)‘𝑦) < (𝑎 + (1 / 𝑗))} = (𝑡 ∩ dom (𝐹‘𝑙))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝑎 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
192 | 158, 159,
160, 161, 191 | cbvmpo 7305 |
. . . 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 43983 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ (𝐺‘𝑦) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷)) |
195 | 1, 2, 42, 126, 194 | issmfled 43965 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |