Step | Hyp | Ref
| Expression |
1 | | n0 3890 |
. . 3
⊢ (𝑆 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑆) |
2 | | metxmet 21949 |
. . . . . . . . 9
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
3 | | metdscn.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
4 | 3 | metdsf 22459 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
5 | 2, 4 | sylan 487 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
6 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝐹:𝑋⟶(0[,]+∞)) |
7 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝐹 Fn 𝑋) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝐹 Fn 𝑋) |
9 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → 𝐹:𝑋⟶(0[,]+∞)) |
10 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → 𝑤 ∈ 𝑋) |
11 | 9, 10 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈ (0[,]+∞)) |
12 | | elxrge0 12152 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) ↔ ((𝐹‘𝑤) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝑤))) |
13 | 12 | simplbi 475 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → (𝐹‘𝑤) ∈
ℝ*) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈
ℝ*) |
15 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → 𝐷 ∈ (Met‘𝑋)) |
16 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
17 | 16 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑋) |
18 | 17 | adantrr 749 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
19 | | metcl 21947 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑧𝐷𝑤) ∈ ℝ) |
20 | 15, 18, 10, 19 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝐷𝑤) ∈ ℝ) |
21 | 12 | simprbi 479 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝑤)) |
22 | 11, 21 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → 0 ≤ (𝐹‘𝑤)) |
23 | 3 | metdsle 22463 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ≤ (𝑧𝐷𝑤)) |
24 | 2, 23 | sylanl1 680 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ≤ (𝑧𝐷𝑤)) |
25 | | xrrege0 11879 |
. . . . . . . . 9
⊢ ((((𝐹‘𝑤) ∈ ℝ* ∧ (𝑧𝐷𝑤) ∈ ℝ) ∧ (0 ≤ (𝐹‘𝑤) ∧ (𝐹‘𝑤) ≤ (𝑧𝐷𝑤))) → (𝐹‘𝑤) ∈ ℝ) |
26 | 14, 20, 22, 24, 25 | syl22anc 1319 |
. . . . . . . 8
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈ ℝ) |
27 | 26 | anassrs 678 |
. . . . . . 7
⊢ ((((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) ∧ 𝑤 ∈ 𝑋) → (𝐹‘𝑤) ∈ ℝ) |
28 | 27 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) → ∀𝑤 ∈ 𝑋 (𝐹‘𝑤) ∈ ℝ) |
29 | | ffnfv 6295 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℝ ↔ (𝐹 Fn 𝑋 ∧ ∀𝑤 ∈ 𝑋 (𝐹‘𝑤) ∈ ℝ)) |
30 | 8, 28, 29 | sylanbrc 695 |
. . . . 5
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑧 ∈ 𝑆) → 𝐹:𝑋⟶ℝ) |
31 | 30 | ex 449 |
. . . 4
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑧 ∈ 𝑆 → 𝐹:𝑋⟶ℝ)) |
32 | 31 | exlimdv 1848 |
. . 3
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (∃𝑧 𝑧 ∈ 𝑆 → 𝐹:𝑋⟶ℝ)) |
33 | 1, 32 | syl5bi 231 |
. 2
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ≠ ∅ → 𝐹:𝑋⟶ℝ)) |
34 | 33 | 3impia 1253 |
1
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹:𝑋⟶ℝ) |