| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bfp.3 | . . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 2 |  | n0 4353 | . . . 4
⊢ (𝑋 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝑋) | 
| 3 | 1, 2 | sylib 218 | . . 3
⊢ (𝜑 → ∃𝑤 𝑤 ∈ 𝑋) | 
| 4 |  | bfp.2 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) | 
| 5 | 4 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝐷 ∈ (CMet‘𝑋)) | 
| 6 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑋 ≠ ∅) | 
| 7 |  | bfp.4 | . . . . 5
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 8 | 7 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝐾 ∈
ℝ+) | 
| 9 |  | bfp.5 | . . . . 5
⊢ (𝜑 → 𝐾 < 1) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝐾 < 1) | 
| 11 |  | bfp.6 | . . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶𝑋) | 
| 12 | 11 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝐹:𝑋⟶𝑋) | 
| 13 |  | bfp.7 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 14 | 13 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 15 |  | eqid 2737 | . . . 4
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) | 
| 16 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋) | 
| 17 |  | eqid 2737 | . . . 4
⊢
seq1((𝐹 ∘
1st ), (ℕ × {𝑤})) = seq1((𝐹 ∘ 1st ), (ℕ ×
{𝑤})) | 
| 18 | 5, 6, 8, 10, 12, 14, 15, 16, 17 | bfplem2 37830 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | 
| 19 | 3, 18 | exlimddv 1935 | . 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | 
| 20 |  | oveq12 7440 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = (𝑥𝐷𝑦)) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = (𝑥𝐷𝑦)) | 
| 22 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 23 | 21, 22 | eqbrtrrd 5167 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝑥𝐷𝑦) ≤ (𝐾 · (𝑥𝐷𝑦))) | 
| 24 |  | cmetmet 25320 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 25 | 4, 24 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 26 | 25 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝐷 ∈ (Met‘𝑋)) | 
| 27 |  | simplrl 777 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝑋) | 
| 28 |  | simplrr 778 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝑦 ∈ 𝑋) | 
| 29 |  | metcl 24342 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ∈ ℝ) | 
| 30 | 26, 27, 28, 29 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝑥𝐷𝑦) ∈ ℝ) | 
| 31 | 7 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 32 | 31 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝐾 ∈ ℝ) | 
| 33 | 32, 30 | remulcld 11291 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝐾 · (𝑥𝐷𝑦)) ∈ ℝ) | 
| 34 | 30, 33 | suble0d 11854 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (((𝑥𝐷𝑦) − (𝐾 · (𝑥𝐷𝑦))) ≤ 0 ↔ (𝑥𝐷𝑦) ≤ (𝐾 · (𝑥𝐷𝑦)))) | 
| 35 | 23, 34 | mpbird 257 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝑥𝐷𝑦) − (𝐾 · (𝑥𝐷𝑦))) ≤ 0) | 
| 36 |  | 1cnd 11256 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 1 ∈ ℂ) | 
| 37 | 32 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝐾 ∈ ℂ) | 
| 38 | 30 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝑥𝐷𝑦) ∈ ℂ) | 
| 39 | 36, 37, 38 | subdird 11720 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((1 − 𝐾) · (𝑥𝐷𝑦)) = ((1 · (𝑥𝐷𝑦)) − (𝐾 · (𝑥𝐷𝑦)))) | 
| 40 | 38 | mullidd 11279 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (1 · (𝑥𝐷𝑦)) = (𝑥𝐷𝑦)) | 
| 41 | 40 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((1 · (𝑥𝐷𝑦)) − (𝐾 · (𝑥𝐷𝑦))) = ((𝑥𝐷𝑦) − (𝐾 · (𝑥𝐷𝑦)))) | 
| 42 | 39, 41 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((1 − 𝐾) · (𝑥𝐷𝑦)) = ((𝑥𝐷𝑦) − (𝐾 · (𝑥𝐷𝑦)))) | 
| 43 |  | 1re 11261 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ | 
| 44 |  | resubcl 11573 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ) → (1 − 𝐾) ∈ ℝ) | 
| 45 | 43, 31, 44 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 − 𝐾) ∈
ℝ) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (1 − 𝐾) ∈ ℝ) | 
| 47 | 46 | recnd 11289 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (1 − 𝐾) ∈ ℂ) | 
| 48 | 47 | mul01d 11460 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((1 − 𝐾) · 0) = 0) | 
| 49 | 35, 42, 48 | 3brtr4d 5175 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((1 − 𝐾) · (𝑥𝐷𝑦)) ≤ ((1 − 𝐾) · 0)) | 
| 50 |  | 0red 11264 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 0 ∈ ℝ) | 
| 51 |  | posdif 11756 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 < 1
↔ 0 < (1 − 𝐾))) | 
| 52 | 31, 43, 51 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐾 < 1 ↔ 0 < (1 − 𝐾))) | 
| 53 | 9, 52 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (1 − 𝐾)) | 
| 54 | 53 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 0 < (1 − 𝐾)) | 
| 55 |  | lemul2 12120 | . . . . . . . . 9
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ 0 ∈ ℝ ∧
((1 − 𝐾) ∈
ℝ ∧ 0 < (1 − 𝐾))) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((1 − 𝐾) · (𝑥𝐷𝑦)) ≤ ((1 − 𝐾) · 0))) | 
| 56 | 30, 50, 46, 54, 55 | syl112anc 1376 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((1 − 𝐾) · (𝑥𝐷𝑦)) ≤ ((1 − 𝐾) · 0))) | 
| 57 | 49, 56 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝑥𝐷𝑦) ≤ 0) | 
| 58 |  | metge0 24355 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥𝐷𝑦)) | 
| 59 | 26, 27, 28, 58 | syl3anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 0 ≤ (𝑥𝐷𝑦)) | 
| 60 |  | 0re 11263 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 61 |  | letri3 11346 | . . . . . . . 8
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦)))) | 
| 62 | 30, 60, 61 | sylancl 586 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦)))) | 
| 63 | 57, 59, 62 | mpbir2and 713 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → (𝑥𝐷𝑦) = 0) | 
| 64 |  | meteq0 24349 | . . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 65 | 26, 27, 28, 64 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 66 | 63, 65 | mpbid 232 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ ((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦)) → 𝑥 = 𝑦) | 
| 67 | 66 | ex 412 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → 𝑥 = 𝑦)) | 
| 68 | 67 | ralrimivva 3202 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → 𝑥 = 𝑦)) | 
| 69 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 70 |  | id 22 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) | 
| 71 | 69, 70 | eqeq12d 2753 | . . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧)) | 
| 72 | 71 | anbi1d 631 | . . . . . 6
⊢ (𝑥 = 𝑧 → (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) ↔ ((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦))) | 
| 73 |  | equequ1 2024 | . . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦)) | 
| 74 | 72, 73 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑧 → ((((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → 𝑥 = 𝑦) ↔ (((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦) → 𝑧 = 𝑦))) | 
| 75 | 74 | ralbidv 3178 | . . . 4
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑋 (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝑋 (((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦) → 𝑧 = 𝑦))) | 
| 76 | 75 | cbvralvw 3237 | . . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (((𝐹‘𝑥) = 𝑥 ∧ (𝐹‘𝑦) = 𝑦) → 𝑥 = 𝑦) ↔ ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦) → 𝑧 = 𝑦)) | 
| 77 | 68, 76 | sylib 218 | . 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦) → 𝑧 = 𝑦)) | 
| 78 |  | fveq2 6906 | . . . 4
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) | 
| 79 |  | id 22 | . . . 4
⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) | 
| 80 | 78, 79 | eqeq12d 2753 | . . 3
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘𝑦) = 𝑦)) | 
| 81 | 80 | reu4 3737 | . 2
⊢
(∃!𝑧 ∈
𝑋 (𝐹‘𝑧) = 𝑧 ↔ (∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧 ∧ ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝐹‘𝑧) = 𝑧 ∧ (𝐹‘𝑦) = 𝑦) → 𝑧 = 𝑦))) | 
| 82 | 19, 77, 81 | sylanbrc 583 | 1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) |