Proof of Theorem metdstri
| Step | Hyp | Ref
| Expression |
| 1 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℝ) |
| 2 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ) |
| 3 | | rexsub 13275 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵))) |
| 4 | 1, 2, 3 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵))) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵)))) |
| 6 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 8 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐵 ∈ 𝑋) |
| 10 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐴 ∈ 𝑋) |
| 12 | 1, 2 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ) |
| 13 | 2 | leidd 11829 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵)) |
| 14 | | xmetsym 24357 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
| 15 | 6, 10, 8, 14 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
| 17 | 16 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵)) |
| 18 | 1 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℂ) |
| 19 | 2 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ) |
| 20 | 18, 19 | nncand 11625 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵)) |
| 21 | 13, 17, 20 | 3brtr4d 5175 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵)))) |
| 22 | | blss2 24414 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 23 | 7, 9, 11, 12, 1, 21, 22 | syl33anc 1387 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 24 | 5, 23 | eqsstrd 4018 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 25 | 24 | expr 456 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) |
| 26 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 27 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ 𝑋) |
| 28 | | metdscn.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
| 29 | 28 | metdsf 24870 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑋⟶(0[,]+∞)) |
| 31 | 30, 10 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈ (0[,]+∞)) |
| 32 | | eliccxr 13475 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈
ℝ*) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈
ℝ*) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹‘𝐴) ∈
ℝ*) |
| 35 | | xmetcl 24341 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
| 36 | 6, 10, 8, 35 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ∈
ℝ*) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈
ℝ*) |
| 38 | 37 | xnegcld 13342 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) →
-𝑒(𝐴𝐷𝐵) ∈
ℝ*) |
| 39 | 34, 38 | xaddcld 13343 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈
ℝ*) |
| 40 | 39 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈
ℝ*) |
| 41 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → +∞ ∈
ℝ*) |
| 43 | | pnfge 13172 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ +∞) |
| 44 | 40, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ +∞) |
| 45 | | ssbl 24433 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋) ∧ (((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞)) |
| 46 | 26, 27, 40, 42, 44, 45 | syl221anc 1383 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞)) |
| 47 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐹‘𝐴) = +∞) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) = (𝐴(ball‘𝐷)+∞)) |
| 49 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐴 ∈ 𝑋) |
| 50 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ) |
| 51 | | xblpnf 24406 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) |
| 52 | 26, 49, 51 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) |
| 53 | 27, 50, 52 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞)) |
| 54 | | blpnfctr 24446 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞)) |
| 55 | 26, 49, 53, 54 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞)) |
| 56 | 48, 55 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 57 | 46, 56 | sseqtrd 4020 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 58 | 57 | expr 456 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) |
| 59 | | elxrge0 13497 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐴))) |
| 60 | 59 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴)) |
| 61 | 31, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐴)) |
| 62 | | ge0nemnf 13215 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐴)) → (𝐹‘𝐴) ≠ -∞) |
| 63 | 33, 61, 62 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≠ -∞) |
| 64 | 33, 63 | jca 511 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞)) |
| 65 | 64 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞)) |
| 66 | | xrnemnf 13159 |
. . . . . . . . 9
⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞) ↔ ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞)) |
| 67 | 65, 66 | sylib 218 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞)) |
| 68 | 25, 58, 67 | mpjaod 861 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 69 | | pnfnlt 13170 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝐴) ∈ ℝ* → ¬
+∞ < (𝐹‘𝐴)) |
| 70 | 33, 69 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ¬ +∞ < (𝐹‘𝐴)) |
| 71 | 70 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ <
(𝐹‘𝐴)) |
| 72 | 36 | xnegcld 13342 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → -𝑒(𝐴𝐷𝐵) ∈
ℝ*) |
| 73 | 33, 72 | xaddcld 13343 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈
ℝ*) |
| 74 | | xbln0 24424 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈ ℝ*) →
((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) |
| 75 | 6, 8, 73, 74 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) |
| 76 | | xposdif 13304 |
. . . . . . . . . . . . 13
⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) |
| 77 | 36, 33, 76 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) |
| 78 | 75, 77 | bitr4d 282 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹‘𝐴))) |
| 79 | | breq1 5146 |
. . . . . . . . . . 11
⊢ ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ +∞ < (𝐹‘𝐴))) |
| 80 | 78, 79 | sylan9bb 509 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹‘𝐴))) |
| 81 | 80 | necon1bbid 2980 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ <
(𝐹‘𝐴) ↔ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) = ∅)) |
| 82 | 71, 81 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) = ∅) |
| 83 | | 0ss 4400 |
. . . . . . . 8
⊢ ∅
⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)) |
| 84 | 82, 83 | eqsstrdi 4028 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 85 | | xmetge0 24354 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
| 86 | 6, 10, 8, 85 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐴𝐷𝐵)) |
| 87 | | ge0nemnf 13215 |
. . . . . . . . . 10
⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤
(𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞) |
| 88 | 36, 86, 87 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≠ -∞) |
| 89 | 36, 88 | jca 511 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞)) |
| 90 | | xrnemnf 13159 |
. . . . . . . 8
⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞)) |
| 91 | 89, 90 | sylib 218 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞)) |
| 92 | 68, 84, 91 | mpjaodan 961 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 93 | | sslin 4243 |
. . . . . 6
⊢ ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) |
| 94 | 92, 93 | syl 17 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) |
| 95 | 33 | xrleidd 13194 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ (𝐹‘𝐴)) |
| 96 | | simplr 769 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝑆 ⊆ 𝑋) |
| 97 | 28 | metdsge 24871 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
| 98 | 6, 96, 10, 33, 97 | syl31anc 1375 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
| 99 | 95, 98 | mpbid 232 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) |
| 100 | | sseq0 4403 |
. . . . 5
⊢ (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) = ∅) |
| 101 | 94, 99, 100 | syl2anc 584 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) = ∅) |
| 102 | 28 | metdsge 24871 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ∈ ℝ*) →
(((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) = ∅)) |
| 103 | 6, 96, 8, 73, 102 | syl31anc 1375 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)))) = ∅)) |
| 104 | 101, 103 | mpbird 257 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵)) |
| 105 | 30, 8 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈ (0[,]+∞)) |
| 106 | | eliccxr 13475 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → (𝐹‘𝐵) ∈
ℝ*) |
| 107 | 105, 106 | syl 17 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈
ℝ*) |
| 108 | | elxrge0 13497 |
. . . . . 6
⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) ↔ ((𝐹‘𝐵) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐵))) |
| 109 | 108 | simprbi 496 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐵)) |
| 110 | 105, 109 | syl 17 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐵)) |
| 111 | | xlesubadd 13305 |
. . . 4
⊢ ((((𝐹‘𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐵) ∈ ℝ*) ∧ (0 ≤
(𝐹‘𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹‘𝐵))) → (((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)))) |
| 112 | 33, 36, 107, 61, 88, 110, 111 | syl33anc 1387 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒
-𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)))) |
| 113 | 104, 112 | mpbid 232 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵))) |
| 114 | | xaddcom 13282 |
. . 3
⊢ (((𝐹‘𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵))) |
| 115 | 107, 36, 114 | syl2anc 584 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵))) |
| 116 | 113, 115 | breqtrd 5169 |
1
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵))) |