| Step | Hyp | Ref
| Expression |
| 1 | | smflimlem2.4 |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 2 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 3 | 1, 2 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
| 4 | 3 | ssrab2f 45122 |
. . 3
⊢ {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐷 |
| 5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐷) |
| 6 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ 𝐷) |
| 7 | | ssrab2 4080 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 8 | 1, 7 | eqsstri 4030 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) |
| 9 | 8 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚)) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑖)) |
| 11 | 10 | iineq1d 45095 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑖 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 12 | 11 | cbviunv 5040 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
| 13 | 12 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∪
𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 14 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) ↔ ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 15 | 13, 14 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 16 | 9, 15 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 17 | 6, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 18 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) |
| 19 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑘 ∈ ℕ |
| 20 | 18, 19 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) |
| 21 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚 𝑖 ∈ 𝑍 |
| 22 | 20, 21 | nfan 1899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) |
| 23 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚𝑥 |
| 24 | | nfii1 5029 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) |
| 25 | 23, 24 | nfel 2920 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) |
| 26 | 22, 25 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 27 | | nfmpt1 5250 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘𝑖) = (ℤ≥‘𝑖) |
| 29 | | uzssz 12899 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 30 | | smflimlem2.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 31 | 30 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑍 ↔ 𝑖 ∈ (ℤ≥‘𝑀)) |
| 32 | 31 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ (ℤ≥‘𝑀)) |
| 33 | 29, 32 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ) |
| 34 | | uzid 12893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
(ℤ≥‘𝑖)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ (ℤ≥‘𝑖)) |
| 36 | 35 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑖 ∈ (ℤ≥‘𝑖)) |
| 37 | | simplll 775 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → (𝜑 ∧ 𝑥 ∈ 𝐷)) |
| 38 | 37 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝜑) |
| 39 | | uzss 12901 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
| 40 | 32, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝑍 → (ℤ≥‘𝑖) ⊆
(ℤ≥‘𝑀)) |
| 41 | 40, 30 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝑍 → (ℤ≥‘𝑖) ⊆ 𝑍) |
| 42 | 41 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑚 ∈ 𝑍) |
| 43 | 42 | ad4ant24 754 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑚 ∈ 𝑍) |
| 44 | | eliinid 45116 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑖)dom (𝐹‘𝑚) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 45 | 44 | adantll 714 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 46 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) |
| 47 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 48 | 46, 47 | fvmpt2d 7029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
| 49 | 48 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
| 50 | | smflimlem2.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 52 | | smflimlem2.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 53 | 52 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
| 55 | 51, 53, 54 | smff 46747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
| 56 | 55 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
| 57 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 58 | 56, 57 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
| 59 | 49, 58 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
| 60 | 38, 43, 45, 59 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
| 61 | 60 | adantl3r 750 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
| 62 | 61 | adantl3r 750 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ) |
| 63 | 1 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
| 64 | 63 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
| 65 | | rabidim2 45107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
| 67 | | climdm 15590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 68 | 66, 67 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐷 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 70 | 69, 67 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ) |
| 71 | 70, 67 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 72 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐹 |
| 73 | | smflimlem2.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 74 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
| 75 | 3, 72, 73, 74 | fnlimfv 45678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
| 76 | 75 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (𝐺‘𝑥)) |
| 77 | 71, 76 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) |
| 78 | 77 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) |
| 79 | | smflimlem2.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 80 | 79 | ad5antr 734 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝐴 ∈ ℝ) |
| 81 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (𝐺‘𝑥) ≤ 𝐴) |
| 82 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑘 ∈ ℕ) |
| 83 | | nnrecrp 45397 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (1 / 𝑘) ∈
ℝ+) |
| 85 | 26, 27, 28, 36, 62, 78, 80, 81, 84 | climleltrp 45691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) |
| 86 | | simp-6l 787 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝜑) |
| 87 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → 𝑖 ∈ 𝑍) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑖 ∈ 𝑍) |
| 89 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 90 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → 𝑛 ∈ (ℤ≥‘𝑖)) |
| 91 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝜑 |
| 92 | 91, 21, 25 | nf3an 1901 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚(𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) |
| 93 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚 𝑛 ∈
(ℤ≥‘𝑖) |
| 94 | 92, 93 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) |
| 95 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚))) |
| 96 | 28 | uztrn2 12897 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈
(ℤ≥‘𝑖) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑖)) |
| 97 | 96 | adantll 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑖)) |
| 98 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑖 ∈ 𝑍) |
| 99 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ (ℤ≥‘𝑖)) |
| 100 | 98, 99, 42 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑚 ∈ 𝑍) |
| 101 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) |
| 102 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍) |
| 103 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 ∈ 𝑍 → ((𝐹‘𝑚)‘𝑥) ∈ V) |
| 104 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
| 105 | 104 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝐹‘𝑚)‘𝑥) ∈ V) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
| 106 | 102, 103,
105 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
| 107 | 106 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ 𝑍 → ((𝐹‘𝑚)‘𝑥) = ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚)) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) = ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚)) |
| 109 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) |
| 110 | 108, 109 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
| 111 | 100, 101,
110 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
| 112 | 44 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ dom (𝐹‘𝑚)) |
| 114 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) |
| 115 | 113, 114 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))) |
| 116 | | rabid 3458 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)))) |
| 117 | 115, 116 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 118 | 111, 117 | syldan 591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 119 | 118 | adantrl 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) ∧ (((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘)))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 120 | 119 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (ℤ≥‘𝑖)) → ((((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 121 | 95, 97, 120 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 122 | 94, 121 | ralimdaa 3260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (∀𝑚 ∈
(ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 123 | 86, 88, 89, 90, 122 | syl31anc 1375 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) ∧ 𝑛 ∈ (ℤ≥‘𝑖)) → (∀𝑚 ∈
(ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 124 | 123 | reximdva 3168 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)(((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) ∈ ℝ ∧ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))‘𝑚) < (𝐴 + (1 / 𝑘))) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 125 | 85, 124 | mpd 15 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 126 | | ssrexv 4053 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥‘𝑖) ⊆ 𝑍 → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 127 | 41, 126 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ 𝑍 → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 128 | 127 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → (∃𝑛 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 129 | 125, 128 | mpd 15 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 130 | 129 | rexlimdva2 3157 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑖 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑖)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))})) |
| 131 | 17, 130 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 132 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) |
| 133 | | nfra1 3284 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} |
| 134 | 132, 133 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 135 | | simpll1 1213 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 136 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
| 137 | 30 | uztrn2 12897 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
| 138 | 137 | ssd 45085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 139 | 138 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 140 | 139 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 141 | 140 | 3adantl1 1167 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 142 | 141 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 143 | | rspa 3248 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
(ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 144 | 143 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 145 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝜑) |
| 146 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 147 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → 𝑘 ∈ ℕ) |
| 148 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
| 149 | 148, 50 | rabexd 5340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 150 | 149 | ralrimivw 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 151 | 150 | ralrimivw 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 152 | 151 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 153 | | smflimlem2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 154 | 153 | elrnmpoid 45233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ ℕ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
| 155 | 146, 147,
152, 154 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) ∈ ran 𝑃) |
| 156 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚𝑃𝑘) ∈ V |
| 157 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝑟 ∈ ran 𝑃 ↔ (𝑚𝑃𝑘) ∈ ran 𝑃)) |
| 158 | 157 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝜑 ∧ 𝑟 ∈ ran 𝑃) ↔ (𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃))) |
| 159 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → (𝐶‘𝑟) = (𝐶‘(𝑚𝑃𝑘))) |
| 160 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 = (𝑚𝑃𝑘) → 𝑟 = (𝑚𝑃𝑘)) |
| 161 | 159, 160 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑟 = (𝑚𝑃𝑘) → ((𝐶‘𝑟) ∈ 𝑟 ↔ (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘))) |
| 162 | 158, 161 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 = (𝑚𝑃𝑘) → (((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) ↔ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)))) |
| 163 | | smflimlem2.10 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
| 164 | 156, 162,
163 | vtocl 3558 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑚𝑃𝑘) ∈ ran 𝑃) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
| 165 | 145, 155,
164 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘)) |
| 166 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) ∈ V) |
| 167 | | smflimlem2.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) |
| 168 | 167 | ovmpt4g 7580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ (𝐶‘(𝑚𝑃𝑘)) ∈ V) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
| 169 | 146, 147,
166, 168 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) = (𝐶‘(𝑚𝑃𝑘))) |
| 170 | 169 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝐶‘(𝑚𝑃𝑘)) = (𝑚𝐻𝑘)) |
| 171 | 145, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) |
| 172 | 153 | ovmpt4g 7580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ∈ V) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 173 | 146, 147,
171, 172 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝑃𝑘) = {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 174 | 170, 173 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ((𝐶‘(𝑚𝑃𝑘)) ∈ (𝑚𝑃𝑘) ↔ (𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})) |
| 175 | 165, 174 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → (𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 176 | | ineq1 4213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑚𝐻𝑘) → (𝑠 ∩ dom (𝐹‘𝑚)) = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚))) |
| 177 | 176 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑚𝐻𝑘) → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
| 178 | 177 | elrab 3692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚𝐻𝑘) ∈ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} ↔ ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
| 179 | 175, 178 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → ((𝑚𝐻𝑘) ∈ 𝑆 ∧ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)))) |
| 180 | 179 | simprd 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚))) |
| 181 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚𝐻𝑘) ∩ dom (𝐹‘𝑚)) ⊆ (𝑚𝐻𝑘) |
| 182 | 180, 181 | eqsstrdi 4028 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘)) |
| 183 | 182 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} ⊆ (𝑚𝐻𝑘)) |
| 184 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) |
| 185 | 183, 184 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ (𝑚𝐻𝑘)) |
| 186 | 135, 136,
142, 144, 185 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ (𝑚𝐻𝑘)) |
| 187 | 186 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → (𝑚 ∈ (ℤ≥‘𝑛) → 𝑥 ∈ (𝑚𝐻𝑘))) |
| 188 | 134, 187 | ralrimi 3257 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘)) |
| 189 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 190 | | eliin 4996 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘))) |
| 191 | 189, 190 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ (𝑚𝐻𝑘)) |
| 192 | 188, 191 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))}) → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 193 | 192 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
| 194 | 193 | ad5ant145 1371 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
| 195 | 194 | reximdva 3168 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
| 196 | 131, 195 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 197 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 198 | 196, 197 | sylibr 234 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 199 | 198 | ralrimiva 3146 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 200 | | eliin 4996 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘))) |
| 201 | 189, 200 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) ↔ ∀𝑘 ∈ ℕ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 202 | 199, 201 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → 𝑥 ∈ ∩
𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘)) |
| 203 | | smflimlem2.9 |
. . . . . 6
⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) |
| 204 | 202, 203 | eleqtrrdi 2852 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ (𝐺‘𝑥) ≤ 𝐴) → 𝑥 ∈ 𝐼) |
| 205 | 204 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
| 206 | 205 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
| 207 | | rabss 4072 |
. . 3
⊢ ({𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐼 ↔ ∀𝑥 ∈ 𝐷 ((𝐺‘𝑥) ≤ 𝐴 → 𝑥 ∈ 𝐼)) |
| 208 | 206, 207 | sylibr 234 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ 𝐼) |
| 209 | 5, 208 | ssind 4241 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ (𝐷 ∩ 𝐼)) |