| Step | Hyp | Ref
| Expression |
| 1 | | relres 6023 |
. . 3
⊢ Rel ( I
↾ 𝑋) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel ( I ↾ 𝑋)) |
| 3 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑞 ∈ V |
| 4 | 3 | brresi 6006 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 I 𝑞)) |
| 5 | | df-br 5144 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) |
| 6 | 3 | ideq 5863 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 I 𝑞 ↔ 𝑝 = 𝑞) |
| 7 | 6 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑝 I 𝑞) ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
| 8 | 4, 5, 7 | 3bitr3i 301 |
. . . . . . . . . . . . 13
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
| 9 | 8 | biimpi 216 |
. . . . . . . . . . . 12
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
| 10 | 9 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝 ∈ 𝑋 ∧ 𝑝 = 𝑞)) |
| 11 | 10 | simprd 495 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 = 𝑞) |
| 12 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑝〉) |
| 13 | | opeq2 4874 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → 〈𝑝, 𝑝〉 = 〈𝑝, 𝑞〉) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑞 → (𝐷‘〈𝑝, 𝑝〉) = (𝐷‘〈𝑝, 𝑞〉)) |
| 15 | 12, 14 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
| 16 | 11, 15 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
| 17 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
| 18 | 10 | simpld 494 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 ∈ 𝑋) |
| 19 | | psmet0 24318 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑝𝐷𝑝) = 0) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = 0) |
| 21 | 16, 20 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) = 0) |
| 22 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 23 | | rpxr 13044 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ∈
ℝ*) |
| 24 | | rpgt0 13047 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 0 < 𝑎) |
| 25 | | lbico1 13441 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 0 <
𝑎) → 0 ∈
(0[,)𝑎)) |
| 26 | 22, 23, 24, 25 | mp3an2i 1468 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ+
→ 0 ∈ (0[,)𝑎)) |
| 27 | 26 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 0 ∈
(0[,)𝑎)) |
| 28 | 21, 27 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) |
| 29 | | psmetf 24316 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 30 | 29 | ffund 6740 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷) |
| 31 | 30 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → Fun 𝐷) |
| 32 | 11, 18 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑞 ∈ 𝑋) |
| 33 | 18, 32 | opelxpd 5724 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
| 34 | 29 | fdmd 6746 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
| 35 | 34 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
| 36 | 33, 35 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ dom 𝐷) |
| 37 | | fvimacnv 7073 |
. . . . . . . 8
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
| 38 | 31, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
| 39 | 28, 38 | mpbid 232 |
. . . . . 6
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
| 40 | 39 | adantr 480 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
| 41 | | simpr 484 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
| 42 | 40, 41 | eleqtrrd 2844 |
. . . 4
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
| 43 | | simplr 769 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 𝐴 ∈ 𝐹) |
| 44 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
| 45 | 44 | metustel 24563 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
| 46 | 45 | ad2antrr 726 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
| 47 | 43, 46 | mpbid 232 |
. . . 4
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
| 48 | 42, 47 | r19.29a 3162 |
. . 3
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
| 49 | 48 | ex 412 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → (〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → 〈𝑝, 𝑞〉 ∈ 𝐴)) |
| 50 | 2, 49 | relssdv 5798 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴) |