Step | Hyp | Ref
| Expression |
1 | | relres 5346 |
. . 3
⊢ Rel ( I
↾ 𝑋) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel ( I ↾ 𝑋)) |
3 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑞 ∈ V |
4 | 3 | brres 5323 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ (𝑝 I 𝑞 ∧ 𝑝 ∈ 𝑋)) |
5 | | df-br 4584 |
. . . . . . . . . . . . . 14
⊢ (𝑝( I ↾ 𝑋)𝑞 ↔ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) |
6 | 3 | ideq 5196 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 I 𝑞 ↔ 𝑝 = 𝑞) |
7 | 6 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 I 𝑞 ∧ 𝑝 ∈ 𝑋) ↔ (𝑝 = 𝑞 ∧ 𝑝 ∈ 𝑋)) |
8 | 4, 5, 7 | 3bitr3i 289 |
. . . . . . . . . . . . 13
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) ↔ (𝑝 = 𝑞 ∧ 𝑝 ∈ 𝑋)) |
9 | 8 | biimpi 205 |
. . . . . . . . . . . 12
⊢
(〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → (𝑝 = 𝑞 ∧ 𝑝 ∈ 𝑋)) |
10 | 9 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝 = 𝑞 ∧ 𝑝 ∈ 𝑋)) |
11 | 10 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 = 𝑞) |
12 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑝〉) |
13 | | opeq2 4341 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑞 → 〈𝑝, 𝑝〉 = 〈𝑝, 𝑞〉) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑞 → (𝐷‘〈𝑝, 𝑝〉) = (𝐷‘〈𝑝, 𝑞〉)) |
15 | 12, 14 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = (𝐷‘〈𝑝, 𝑞〉)) |
17 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
18 | 10 | simprd 478 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑝 ∈ 𝑋) |
19 | | psmet0 21923 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑝𝐷𝑝) = 0) |
20 | 17, 18, 19 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝑝𝐷𝑝) = 0) |
21 | 16, 20 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) = 0) |
22 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 0 ∈ ℝ*) |
24 | | rpxr 11716 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ∈
ℝ*) |
25 | | rpgt0 11720 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ+
→ 0 < 𝑎) |
26 | | lbico1 12099 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 0 <
𝑎) → 0 ∈
(0[,)𝑎)) |
27 | 23, 24, 25, 26 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ+
→ 0 ∈ (0[,)𝑎)) |
28 | 27 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 0 ∈
(0[,)𝑎)) |
29 | 21, 28 | eqeltrd 2688 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) |
30 | | psmetf 21921 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
31 | | ffun 5961 |
. . . . . . . . . 10
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun
𝐷) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷) |
33 | 32 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → Fun 𝐷) |
34 | 11, 18 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → 𝑞 ∈ 𝑋) |
35 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
36 | 18, 34, 35 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
37 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
38 | 30, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
39 | 38 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
40 | 36, 39 | eleqtrrd 2691 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ dom 𝐷) |
41 | | fvimacnv 6240 |
. . . . . . . 8
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
42 | 33, 40, 41 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
43 | 29, 42 | mpbid 221 |
. . . . . 6
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) →
〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
44 | 43 | adantr 480 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
45 | | simpr 476 |
. . . . 5
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
46 | 44, 45 | eleqtrrd 2691 |
. . . 4
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
47 | | simplr 788 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 𝐴 ∈ 𝐹) |
48 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
49 | 48 | metustel 22165 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
50 | 49 | ad2antrr 758 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
51 | 47, 50 | mpbid 221 |
. . . 4
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
52 | 46, 51 | r19.29a 3060 |
. . 3
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋)) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
53 | 52 | ex 449 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → (〈𝑝, 𝑞〉 ∈ ( I ↾ 𝑋) → 〈𝑝, 𝑞〉 ∈ 𝐴)) |
54 | 2, 53 | relssdv 5135 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴) |