Proof of Theorem metds0
Step | Hyp | Ref
| Expression |
1 | | metdscn.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
2 | 1 | metdsf 22459 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
3 | 2 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐹:𝑋⟶(0[,]+∞)) |
4 | | ssel2 3563 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
5 | 4 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
6 | 3, 5 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ∈ (0[,]+∞)) |
7 | | elxrge0 12152 |
. . . . . . . 8
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐴))) |
8 | 7 | simplbi 475 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈
ℝ*) |
9 | 6, 8 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ∈
ℝ*) |
10 | | xrleid 11859 |
. . . . . 6
⊢ ((𝐹‘𝐴) ∈ ℝ* → (𝐹‘𝐴) ≤ (𝐹‘𝐴)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) ≤ (𝐹‘𝐴)) |
12 | | simp1 1054 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝐷 ∈ (∞Met‘𝑋)) |
13 | | simp2 1055 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 𝑆 ⊆ 𝑋) |
14 | 1 | metdsge 22460 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
15 | 12, 13, 5, 9, 14 | syl31anc 1321 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)) |
16 | 11, 15 | mpbid 221 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) |
17 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑆) |
18 | 12 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐷 ∈ (∞Met‘𝑋)) |
19 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑋) |
20 | 9 | adantr 480 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → (𝐹‘𝐴) ∈
ℝ*) |
21 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 0 < (𝐹‘𝐴)) |
22 | | xblcntr 22026 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 <
(𝐹‘𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
23 | 18, 19, 20, 21, 22 | syl112anc 1322 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) |
24 | | inelcm 3984 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴))) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅) |
25 | 17, 23, 24 | syl2anc 691 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) ∧ 0 < (𝐹‘𝐴)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅) |
26 | 25 | ex 449 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 < (𝐹‘𝐴) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ≠ ∅)) |
27 | 26 | necon2bd 2798 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ((𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅ → ¬ 0 < (𝐹‘𝐴))) |
28 | 16, 27 | mpd 15 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → ¬ 0 < (𝐹‘𝐴)) |
29 | 7 | simprbi 479 |
. . . . . 6
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴)) |
30 | 6, 29 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝐹‘𝐴)) |
31 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
32 | | xrleloe 11853 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → (0 ≤
(𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
33 | 31, 9, 32 | sylancr 694 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
34 | 30, 33 | mpbid 221 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))) |
35 | 34 | ord 391 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (¬ 0 < (𝐹‘𝐴) → 0 = (𝐹‘𝐴))) |
36 | 28, 35 | mpd 15 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → 0 = (𝐹‘𝐴)) |
37 | 36 | eqcomd 2616 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) = 0) |