| Step | Hyp | Ref
| Expression |
| 1 | | bfp.2 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) |
| 2 | | cmetmet 25320 |
. . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
| 4 | | metxmet 24344 |
. . . 4
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 5 | | bfp.8 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
| 6 | 5 | mopntopon 24449 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
| 7 | 3, 4, 6 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 8 | | bfp.3 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 9 | | bfp.4 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
| 10 | | bfp.5 |
. . . 4
⊢ (𝜑 → 𝐾 < 1) |
| 11 | | bfp.6 |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶𝑋) |
| 12 | | bfp.7 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) |
| 13 | | bfp.9 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 14 | | bfp.10 |
. . . 4
⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ ×
{𝐴})) |
| 15 | 1, 8, 9, 10, 11, 12, 5, 13, 14 | bfplem1 37829 |
. . 3
⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) |
| 16 | | lmcl 23305 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) →
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) |
| 17 | 7, 15, 16 | syl2anc 584 |
. 2
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) |
| 18 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) |
| 19 | 18, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (∞Met‘𝑋)) |
| 20 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 21 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℤ) |
| 22 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
| 23 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) |
| 24 | | rphalfcl 13062 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
| 25 | 24 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
| 26 | 5, 19, 20, 21, 22, 23, 25 | lmmcvg 25295 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 27 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) |
| 28 | 27 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) |
| 29 | | nnz 12634 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
| 31 | | uzid 12893 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 32 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → (𝐺‘𝑘) = (𝐺‘𝑗)) |
| 33 | 32 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 34 | 33 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 35 | 34 | rspcv 3618 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 36 | 30, 31, 35 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 37 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 38 | | peano2uz 12943 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 39 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑗 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑗 + 1))) |
| 40 | 39 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑗 + 1) → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 41 | 40 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑗 + 1) → (((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 42 | 41 | rspcv 3618 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 + 1) ∈
(ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 43 | 37, 38, 42 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 44 | | 1zzd 12648 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℤ) |
| 45 | 20, 14, 44, 13, 11 | algrp1 16611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (𝐹‘(𝐺‘𝑗))) |
| 46 | 45 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (𝐹‘(𝐺‘𝑗))) |
| 47 | 46 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 48 | 47 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 49 | 43, 48 | sylibd 239 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))) |
| 50 | 36, 49 | jcad 512 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))) |
| 51 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) |
| 52 | 20, 14, 44, 13, 11 | algrf 16610 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:ℕ⟶𝑋) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐺:ℕ⟶𝑋) |
| 54 | 53 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ 𝑋) |
| 55 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) |
| 56 | | metcl 24342 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑗) ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 57 | 51, 54, 55, 56 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 58 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐹:𝑋⟶𝑋) |
| 59 | 58, 54 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝐺‘𝑗)) ∈ 𝑋) |
| 60 | | metcl 24342 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 61 | 51, 59, 55, 60 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 62 | | rpre 13043 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 63 | 62 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈
ℝ) |
| 64 | | lt2halves 12501 |
. . . . . . . . . . . . 13
⊢ ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥)) |
| 65 | 57, 61, 63, 64 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥)) |
| 66 | 11, 17 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋) |
| 67 | | metcl 24342 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 68 | 3, 66, 17, 67 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ) |
| 70 | 58, 55 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋) |
| 71 | | metcl 24342 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ) |
| 72 | 51, 59, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ) |
| 73 | 72, 61 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ) |
| 74 | 57, 61 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ) |
| 75 | | mettri2 24351 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 76 | 51, 59, 70, 55, 75 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 77 | 9 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 78 | 77 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐾 ∈
ℝ) |
| 79 | 78, 57 | remulcld 11291 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ) |
| 80 | 54, 55 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗) ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)) |
| 81 | 12 | ralrimivva 3202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) |
| 82 | 81 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) |
| 83 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝐺‘𝑗) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑗))) |
| 84 | 83 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝐺‘𝑗) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦))) |
| 85 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝐺‘𝑗) → (𝑥𝐷𝑦) = ((𝐺‘𝑗)𝐷𝑦)) |
| 86 | 85 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝐺‘𝑗) → (𝐾 · (𝑥𝐷𝑦)) = (𝐾 · ((𝐺‘𝑗)𝐷𝑦))) |
| 87 | 84, 86 | breq12d 5156 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝐺‘𝑗) → (((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑗)𝐷𝑦)))) |
| 88 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 =
((⇝𝑡‘𝐽)‘𝐺) → (𝐹‘𝑦) = (𝐹‘((⇝𝑡‘𝐽)‘𝐺))) |
| 89 | 88 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 =
((⇝𝑡‘𝐽)‘𝐺) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺)))) |
| 90 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 =
((⇝𝑡‘𝐽)‘𝐺) → ((𝐺‘𝑗)𝐷𝑦) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 91 | 90 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 =
((⇝𝑡‘𝐽)‘𝐺) → (𝐾 · ((𝐺‘𝑗)𝐷𝑦)) = (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 92 | 89, 91 | breq12d 5156 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 =
((⇝𝑡‘𝐽)‘𝐺) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑗)𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))))) |
| 93 | 87, 92 | rspc2v 3633 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑗) ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))))) |
| 94 | 80, 82, 93 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 95 | | 1red 11262 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 1 ∈
ℝ) |
| 96 | | metge0 24355 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑗) ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → 0 ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 97 | 51, 54, 55, 96 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 0 ≤
((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 98 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ |
| 99 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 < 1
→ 𝐾 ≤
1)) |
| 100 | 77, 98, 99 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 < 1 → 𝐾 ≤ 1)) |
| 101 | 10, 100 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ≤ 1) |
| 102 | 101 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐾 ≤ 1) |
| 103 | 78, 95, 57, 97, 102 | lemul1ad 12207 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ (1 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 104 | 57 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℂ) |
| 105 | 104 | mullidd 11279 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (1
· ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 106 | 103, 105 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 107 | 72, 79, 57, 94, 106 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 108 | 72, 57, 61, 107 | leadd1dd 11877 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 109 | 69, 73, 74, 76, 108 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)))) |
| 110 | | lelttr 11351 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 111 | 69, 74, 63, 110 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 112 | 109, 111 | mpand 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 113 | 50, 65, 112 | 3syld 60 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 114 | 28, 113 | syl5 34 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 115 | 114 | rexlimdva 3155 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)) |
| 116 | 26, 115 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥) |
| 117 | | ltle 11349 |
. . . . . . . . 9
⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥)) |
| 118 | 68, 62, 117 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥)) |
| 119 | 116, 118 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥) |
| 120 | 62 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
| 121 | 120 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
| 122 | 121 | addlidd 11462 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (0 +
𝑥) = 𝑥) |
| 123 | 119, 122 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥)) |
| 124 | 123 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥)) |
| 125 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 126 | | alrple 13248 |
. . . . . 6
⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 0 ∈ ℝ) →
(((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥))) |
| 127 | 68, 125, 126 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥))) |
| 128 | 124, 127 | mpbird 257 |
. . . 4
⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0) |
| 129 | | metge0 24355 |
. . . . 5
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 130 | 3, 66, 17, 129 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺))) |
| 131 | | letri3 11346 |
. . . . 5
⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 0 ∈ ℝ) →
(((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ∧ 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺))))) |
| 132 | 68, 125, 131 | sylancl 586 |
. . . 4
⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ∧ 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺))))) |
| 133 | 128, 130,
132 | mpbir2and 713 |
. . 3
⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0) |
| 134 | | meteq0 24349 |
. . . 4
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺))) |
| 135 | 3, 66, 17, 134 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺))) |
| 136 | 133, 135 | mpbid 232 |
. 2
⊢ (𝜑 → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)) |
| 137 | | fveq2 6906 |
. . . 4
⊢ (𝑧 =
((⇝𝑡‘𝐽)‘𝐺) → (𝐹‘𝑧) = (𝐹‘((⇝𝑡‘𝐽)‘𝐺))) |
| 138 | | id 22 |
. . . 4
⊢ (𝑧 =
((⇝𝑡‘𝐽)‘𝐺) → 𝑧 = ((⇝𝑡‘𝐽)‘𝐺)) |
| 139 | 137, 138 | eqeq12d 2753 |
. . 3
⊢ (𝑧 =
((⇝𝑡‘𝐽)‘𝐺) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺))) |
| 140 | 139 | rspcev 3622 |
. 2
⊢
((((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) |
| 141 | 17, 136, 140 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) |