Proof of Theorem metds0
| Step | Hyp | Ref
| Expression |
| 1 | | metdscn.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
| 2 | 1 | metdsf 24870 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
| 3 | 2 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐹:𝑋⟶(0[,]+∞)) |
| 4 | | ssel2 3978 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
| 5 | 4 | 3adant1 1131 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
| 6 | 3, 5 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ∈ (0[,]+∞)) |
| 7 | | eliccxr 13475 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈
ℝ*) |
| 8 | 6, 7 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ∈
ℝ*) |
| 9 | 8 | xrleidd 13194 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ≤ (𝐹‘𝐴)) |
| 10 | | simp1 1137 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐷 ∈ (∞Met‘𝑋)) |
| 11 | | simp2 1138 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
| 12 | 1 | metdsge 24871 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
| 13 | 10, 11, 5, 8, 12 | syl31anc 1375 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
| 14 | 9, 13 | mpbid 232 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) |
| 15 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑆) |
| 16 | 10 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 17 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑋) |
| 18 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → (𝐹‘𝐴) ∈
ℝ*) |
| 19 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 0 < (𝐹‘𝐴)) |
| 20 | | xblcntr 24421 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 <
(𝐹‘𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 21 | 16, 17, 18, 19, 20 | syl112anc 1376 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
| 22 | | inelcm 4465 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅) |
| 23 | 15, 21, 22 | syl2anc 584 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅) |
| 24 | 23 | ex 412 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 < (𝐹‘𝐴) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅)) |
| 25 | 24 | necon2bd 2956 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ((𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅ → ¬ 0 < (𝐹‘𝐴))) |
| 26 | 14, 25 | mpd 15 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ¬ 0 < (𝐹‘𝐴)) |
| 27 | | elxrge0 13497 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐴))) |
| 28 | 27 | simprbi 496 |
. . . . . 6
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴)) |
| 29 | 6, 28 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝐹‘𝐴)) |
| 30 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 31 | | xrleloe 13186 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → (0 ≤
(𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
| 32 | 30, 8, 31 | sylancr 587 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
| 33 | 29, 32 | mpbid 232 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))) |
| 34 | 33 | ord 865 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (¬ 0 < (𝐹‘𝐴) → 0 = (𝐹‘𝐴))) |
| 35 | 26, 34 | mpd 15 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 0 = (𝐹‘𝐴)) |
| 36 | 35 | eqcomd 2743 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) = 0) |