Step | Hyp | Ref
| Expression |
1 | | relres 5920 |
. . 3
⊢ Rel ( I
↾ 𝑋) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel ( I ↾ 𝑋)) |
3 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑞 ∈ V |
4 | 3 | brresi 5900 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 I 𝑞)) |
5 | | df-br 5075 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) |
6 | 3 | ideq 5761 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 I 𝑞 ↔ 𝑝 = 𝑞) |
7 | 6 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑝 I 𝑞) ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
8 | 4, 5, 7 | 3bitr3i 301 |
. . . . . . . . . . . . 13
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
9 | 8 | biimpi 215 |
. . . . . . . . . . . 12
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
10 | 9 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
11 | 10 | simprd 496 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 = 𝑞) |
12 | | df-ov 7278 |
. . . . . . . . . . 11
⊢ (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑝〉) |
13 | | opeq2 4805 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → 〈𝑝, 𝑝〉 = 〈𝑝, 𝑞〉) |
14 | 13 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑞 → (𝐷‘〈𝑝, 𝑝〉) = (𝐷‘〈𝑝, 𝑞〉)) |
15 | 12, 14 | eqtrid 2790 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
17 | | simplll 772 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
18 | 10 | simpld 495 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 ∈ 𝑋) |
19 | | psmet0 23461 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑝𝐷𝑝) = 0) |
20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = 0) |
21 | 16, 20 | eqtr3d 2780 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) = 0) |
22 | | 0xr 11022 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
23 | | rpxr 12739 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ∈
ℝ*) |
24 | | rpgt0 12742 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 0 < 𝑎) |
25 | | lbico1 13133 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 0 <
𝑎) → 0 ∈
(0[,)𝑎)) |
26 | 22, 23, 24, 25 | mp3an2i 1465 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ+
→ 0 ∈ (0[,)𝑎)) |
27 | 26 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 0 ∈
(0[,)𝑎)) |
28 | 21, 27 | eqeltrd 2839 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) |
29 | | psmetf 23459 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
30 | 29 | ffund 6604 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷) |
31 | 30 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → Fun 𝐷) |
32 | 11, 18 | eqeltrrd 2840 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑞 ∈ 𝑋) |
33 | 18, 32 | opelxpd 5627 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
34 | 29 | fdmd 6611 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
35 | 34 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
36 | 33, 35 | eleqtrrd 2842 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ dom 𝐷) |
37 | | fvimacnv 6930 |
. . . . . . . 8
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
38 | 31, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
39 | 28, 38 | mpbid 231 |
. . . . . 6
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
40 | 39 | adantr 481 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
41 | | simpr 485 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
42 | 40, 41 | eleqtrrd 2842 |
. . . 4
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
43 | | simplr 766 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 𝐴 ∈ 𝐹) |
44 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
45 | 44 | metustel 23706 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
46 | 45 | ad2antrr 723 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
47 | 43, 46 | mpbid 231 |
. . . 4
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
48 | 42, 47 | r19.29a 3218 |
. . 3
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
49 | 48 | ex 413 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → (〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → 〈𝑝, 𝑞〉 ∈ 𝐴)) |
50 | 2, 49 | relssdv 5698 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴) |