Step | Hyp | Ref
| Expression |
1 | | smflimlem2.4 |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
2 | | nfrab1 3099 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
3 | 1, 2 | nfcxfr 2749 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
4 | 3 | ssrab2f 38331 |
. . 3
⊢ {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐷 |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐷) |
6 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ 𝐷) |
7 | | ssrab2 3650 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
8 | 1, 7 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
9 | 8 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
10 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
11 | 10 | iineq1d 38295 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
12 | 11 | cbviunv 4495 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
13 | 12 | eleq2i 2680 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
14 | | eliun 4460 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ↔ ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
15 | 13, 14 | bitri 263 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
16 | 9, 15 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
18 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) |
19 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚 𝑘 ∈ ℕ |
20 | 18, 19 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚(((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) |
21 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑖 ∈ 𝑍 |
22 | 20, 21 | nfan 1816 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) |
23 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝑥 |
24 | | nfii1 4487 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
25 | 23, 24 | nfel 2763 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) |
26 | 22, 25 | nfan 1816 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
27 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
28 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
29 | | uzssz 11583 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
30 | | smflimlem2.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 =
(ℤ≥‘𝑀) |
31 | 30 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝑍 ↔ 𝑖 ∈ (ℤ≥‘𝑀)) |
32 | 31 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ (ℤ≥‘𝑀)) |
33 | 29, 32 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ) |
34 | | uzid 11578 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ (ℤ≥‘𝑖)) |
36 | 35 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑖 ∈ (ℤ≥‘𝑖)) |
37 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → (𝜑 ∧ 𝑥 ∈ 𝐷)) |
38 | 37 | simpld 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝜑) |
39 | | uzss 11584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
40 | 32, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝑍 → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
41 | 40, 30 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝑍 → (ℤ≥‘𝑖) ⊆ 𝑍) |
42 | 41 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑚 ∈ 𝑍) |
43 | 42 | ad4ant24 1290 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑚 ∈ 𝑍) |
44 | | eliinid 38325 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
45 | 44 | adantll 746 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
46 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
47 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑚)‘𝑥) ∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
49 | 46, 48 | fvmpt2d 6202 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
50 | 49 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
51 | | smflimlem2.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑆 ∈ SAlg) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
53 | | smflimlem2.3 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
54 | 53 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
55 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
56 | 52, 54, 55 | smff 39618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
57 | 56 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
58 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
59 | 57, 58 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
60 | 50, 59 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
61 | 38, 43, 45, 60 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
62 | 61 | ad5ant1345 1308 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
63 | 62 | ad5ant1345 1308 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
64 | 1 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
65 | 64 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
66 | | rabidim2 38313 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐷 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
68 | | climdm 14133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
69 | 67, 68 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
71 | 70, 68 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
72 | 71, 68 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
73 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐹 |
74 | | smflimlem2.5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
75 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
76 | 3, 73, 74, 75 | fnlimfv 38730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
77 | 76 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (𝐺‘𝑥)) |
78 | 72, 77 | breqtrd 4609 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) |
79 | 78 | ad4antr 764 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) |
80 | | smflimlem2.6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℝ) |
81 | 80 | ad5antr 766 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝐴 ∈ ℝ) |
82 | | simp-4r 803 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (𝐺‘𝑥) ≤ 𝐴) |
83 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑘 ∈ ℕ) |
84 | | nnrecrp 38546 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (1 / 𝑘) ∈
ℝ+) |
86 | 26, 27, 28, 36, 63, 79, 81, 82, 85 | climleltrp 38743 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) |
87 | | simp-6l 806 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
88 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑖 ∈ 𝑍) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑖 ∈ 𝑍) |
90 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
91 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ (ℤ≥‘𝑖)) |
92 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚𝜑 |
93 | 92, 21, 25 | nf3an 1819 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚(𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
94 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚 𝑛 ∈
(ℤ≥‘𝑖) |
95 | 93, 94 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) |
96 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚))) |
97 | 28 | uztrn2 11581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑖)) |
98 | 97 | adantll 746 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑖)) |
99 | | simpll2 1094 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑖 ∈ 𝑍) |
100 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ (ℤ≥‘𝑖)) |
101 | 99, 100, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ 𝑍) |
102 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) |
103 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍) |
104 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ 𝑍 → ((𝐹‘𝑚)‘𝑥) ∈ V) |
105 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
106 | 105 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝐹‘𝑚)‘𝑥) ∈ V) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
107 | 103, 104,
106 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
108 | 107 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ 𝑍 → ((𝐹‘𝑚)‘𝑥) = ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚)) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) = ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚)) |
110 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) |
111 | 109, 110 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
112 | 101, 102,
111 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
113 | 44 | 3ad2antl3 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ dom (𝐹‘𝑚)) |
115 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
116 | 114, 115 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))) |
117 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))) |
118 | 116, 117 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
119 | 112, 118 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
120 | 119 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ (((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
121 | 120 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
122 | 96, 98, 121 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
123 | 95, 122 | ralimdaa 2941 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (∀𝑚 ∈
(ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
124 | 87, 89, 90, 91, 123 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (∀𝑚 ∈
(ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
125 | 124 | reximdva 3000 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
126 | 86, 125 | mpd 15 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
127 | | ssrexv 3630 |
. . . . . . . . . . . . . . . 16
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
128 | 41, 127 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑍 → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
129 | 128 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
130 | 126, 129 | mpd 15 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
131 | 130 | ex 449 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
132 | 131 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
133 | 17, 132 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
134 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) |
135 | | nfra1 2925 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} |
136 | 134, 135 | nfan 1816 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
137 | | simpll1 1093 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
138 | | simpll2 1094 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
139 | 30 | uztrn2 11581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
140 | 139 | ssd 38278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ⊆ 𝑍) |
141 | 140 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
142 | 141 | adantll 746 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
143 | 142 | 3adantl1 1210 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
144 | 143 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
145 | | rspa 2914 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
(ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
146 | 145 | adantll 746 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
147 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝜑) |
148 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
149 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑘 ∈ ℕ) |
150 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
151 | 150, 51 | rabexd 4741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
152 | 151 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
153 | 152 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
154 | 153 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
155 | | smflimlem2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
156 | 155 | elrnmpt2id 38422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
157 | 148, 149,
154, 156 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
158 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚𝑃𝑘) ∈ V |
159 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝑟 ∈ ran 𝑃 ↔ (𝑚𝑃𝑘) ∈ ran 𝑃)) |
160 | 159 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝜑 ∧ 𝑟 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃))) |
161 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝐶‘𝑟) = (𝐶‘(𝑚𝑃𝑘))) |
162 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → 𝑟 = (𝑚𝑃𝑘)) |
163 | 161, 162 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝐶‘𝑟) ∈ 𝑟 ↔ (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))) |
164 | 160, 163 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 = (𝑚𝑃𝑘) → (((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) ↔ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)))) |
165 | | smflimlem2.10 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
166 | 158, 164,
165 | vtocl 3232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
167 | 147, 157,
166 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
168 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶‘(𝑚𝑃𝑘)) ∈ V |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ V) |
170 | | smflimlem2.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) |
171 | 170 | ovmpt4g 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ (𝐶‘(𝑚𝑃𝑘)) ∈ V) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
172 | 148, 149,
169, 171 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
173 | 172 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) = (𝑚𝐻𝑘)) |
174 | 147, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
175 | 155 | ovmpt4g 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
176 | 148, 149,
174, 175 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
177 | 173, 176 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ((𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘) ↔ (𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})) |
178 | 167, 177 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
179 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑚𝐻𝑘) → (𝑠 ∩ dom (𝐹‘𝑚)) = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚))) |
180 | 179 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑚𝐻𝑘) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
181 | 180 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ↔ ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
182 | 178, 181 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
183 | 182 | simprd 478 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚))) |
184 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)) ⊆ (𝑚𝐻𝑘) |
185 | 183, 184 | syl6eqss 3618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘)) |
186 | 185 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘)) |
187 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
188 | 186, 187 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ (𝑚𝐻𝑘)) |
189 | 137, 138,
144, 146, 188 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ (𝑚𝐻𝑘)) |
190 | 189 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → (𝑚 ∈ (ℤ≥‘𝑛) → 𝑥 ∈ (𝑚𝐻𝑘))) |
191 | 136, 190 | ralrimi 2940 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘)) |
192 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
193 | | eliin 4461 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘))) |
194 | 192, 193 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘)) |
195 | 191, 194 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
196 | 195 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
197 | 196 | ad5ant145 1307 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
198 | 197 | reximdva 3000 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
199 | 133, 198 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
200 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
201 | 199, 200 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
202 | 201 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
203 | | eliin 4461 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
204 | 192, 203 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
205 | 202, 204 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → 𝑥 ∈ ∩
𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
206 | | smflimlem2.9 |
. . . . . 6
⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) |
207 | 205, 206 | syl6eleqr 2699 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → 𝑥 ∈ 𝐼) |
208 | 207 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
209 | 208 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
210 | | rabss 3642 |
. . 3
⊢ ({𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐼 ↔ ∀𝑥 ∈ 𝐷 ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
211 | 209, 210 | sylibr 223 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐼) |
212 | 5, 211 | ssind 3799 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ (𝐷 ∩ 𝐼)) |