Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
2 | 1 | metustel 22355 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎)))) |
3 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
4 | | cnvimass 5485 |
. . . . . . . . . 10
⊢ (◡𝐷 “ (0[,)𝑎)) ⊆ dom 𝐷 |
5 | | psmetf 22111 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
6 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → dom 𝐷 = (𝑋 × 𝑋)) |
9 | 4, 8 | syl5sseq 3653 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋)) |
10 | 3, 9 | eqsstrd 3639 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → 𝑥 ⊆ (𝑋 × 𝑋)) |
11 | 10 | ex 450 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 = (◡𝐷 “ (0[,)𝑎)) → 𝑥 ⊆ (𝑋 × 𝑋))) |
12 | 11 | rexlimdvw 3034 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎)) → 𝑥 ⊆ (𝑋 × 𝑋))) |
13 | 2, 12 | sylbid 230 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ⊆ (𝑋 × 𝑋))) |
14 | 13 | ralrimiv 2965 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝐹 𝑥 ⊆ (𝑋 × 𝑋)) |
15 | | pwssb 4612 |
. . . 4
⊢ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∀𝑥 ∈ 𝐹 𝑥 ⊆ (𝑋 × 𝑋)) |
16 | 14, 15 | sylibr 224 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐹 ⊆ 𝒫 (𝑋 × 𝑋)) |
17 | 16 | adantl 482 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ⊆ 𝒫 (𝑋 × 𝑋)) |
18 | | cnvexg 7112 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → ◡𝐷 ∈ V) |
19 | | imaexg 7103 |
. . . . . . 7
⊢ (◡𝐷 ∈ V → (◡𝐷 “ (0[,)1)) ∈ V) |
20 | | elisset 3215 |
. . . . . . 7
⊢ ((◡𝐷 “ (0[,)1)) ∈ V →
∃𝑥 𝑥 = (◡𝐷 “ (0[,)1))) |
21 | | 1rp 11836 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
22 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → (0[,)𝑎) = (0[,)1)) |
23 | 22 | imaeq2d 5466 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)1))) |
24 | 23 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (𝑥 = (◡𝐷 “ (0[,)𝑎)) ↔ 𝑥 = (◡𝐷 “ (0[,)1)))) |
25 | 24 | rspcev 3309 |
. . . . . . . . 9
⊢ ((1
∈ ℝ+ ∧ 𝑥 = (◡𝐷 “ (0[,)1))) → ∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎))) |
26 | 21, 25 | mpan 706 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐷 “ (0[,)1)) → ∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎))) |
27 | 26 | eximi 1762 |
. . . . . . 7
⊢
(∃𝑥 𝑥 = (◡𝐷 “ (0[,)1)) → ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
28 | 18, 19, 20, 27 | 4syl 19 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
29 | 2 | exbidv 1850 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (∃𝑥 𝑥 ∈ 𝐹 ↔ ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎)))) |
30 | 28, 29 | mpbird 247 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 𝑥 ∈ 𝐹) |
31 | 30 | adantl 482 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 𝑥 ∈ 𝐹) |
32 | | n0 3931 |
. . . 4
⊢ (𝐹 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐹) |
33 | 31, 32 | sylibr 224 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ≠ ∅) |
34 | 1 | metustid 22359 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝑥) |
35 | 34 | adantll 750 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝑥) |
36 | | n0 3931 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ ↔
∃𝑝 𝑝 ∈ 𝑋) |
37 | 36 | biimpi 206 |
. . . . . . . . 9
⊢ (𝑋 ≠ ∅ →
∃𝑝 𝑝 ∈ 𝑋) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑝 𝑝 ∈ 𝑋) |
39 | | opelresi 5408 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ 𝑋 → (〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋) ↔ 𝑝 ∈ 𝑋)) |
40 | 39 | ibir 257 |
. . . . . . . . . 10
⊢ (𝑝 ∈ 𝑋 → 〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋)) |
41 | | ne0i 3921 |
. . . . . . . . . 10
⊢
(〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (𝑝 ∈ 𝑋 → ( I ↾ 𝑋) ≠ ∅) |
43 | 42 | exlimiv 1858 |
. . . . . . . 8
⊢
(∃𝑝 𝑝 ∈ 𝑋 → ( I ↾ 𝑋) ≠ ∅) |
44 | 38, 43 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ( I ↾ 𝑋) ≠ ∅) |
45 | 44 | adantr 481 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ≠ ∅) |
46 | | ssn0 3976 |
. . . . . 6
⊢ ((( I
↾ 𝑋) ⊆ 𝑥 ∧ ( I ↾ 𝑋) ≠ ∅) → 𝑥 ≠ ∅) |
47 | 35, 45, 46 | syl2anc 693 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ≠ ∅) |
48 | 47 | nelrdva 3417 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ¬ ∅ ∈
𝐹) |
49 | | df-nel 2898 |
. . . 4
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
50 | 48, 49 | sylibr 224 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∅ ∉ 𝐹) |
51 | | df-ss 3588 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∩ 𝑦) = 𝑥) |
52 | 51 | biimpi 206 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∩ 𝑦) = 𝑥) |
53 | 52 | adantl 482 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∩ 𝑦) = 𝑥) |
54 | | simplrl 800 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ 𝐹) |
55 | 53, 54 | eqeltrd 2701 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
56 | | sseqin2 3817 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝑥 ↔ (𝑥 ∩ 𝑦) = 𝑦) |
57 | 56 | biimpi 206 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝑥 → (𝑥 ∩ 𝑦) = 𝑦) |
58 | 57 | adantl 482 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∩ 𝑦) = 𝑦) |
59 | | simplrr 801 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ 𝐹) |
60 | 58, 59 | eqeltrd 2701 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
61 | | simplr 792 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝐷 ∈ (PsMet‘𝑋)) |
62 | | simprl 794 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝑥 ∈ 𝐹) |
63 | | simprr 796 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝑦 ∈ 𝐹) |
64 | 1 | metustto 22358 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) |
65 | 61, 62, 63, 64 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) |
66 | 55, 60, 65 | mpjaodan 827 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
67 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
68 | 67 | inex1 4799 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ∈ V |
69 | 68 | pwid 4174 |
. . . . . . 7
⊢ (𝑥 ∩ 𝑦) ∈ 𝒫 (𝑥 ∩ 𝑦) |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝒫 (𝑥 ∩ 𝑦)) |
71 | 70 | elpwid 4170 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) |
72 | | sseq1 3626 |
. . . . . 6
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
73 | 72 | rspcev 3309 |
. . . . 5
⊢ (((𝑥 ∩ 𝑦) ∈ 𝐹 ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
74 | 66, 71, 73 | syl2anc 693 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
75 | 74 | ralrimivva 2971 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
76 | 33, 50, 75 | 3jca 1242 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
77 | | elfvex 6221 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V) |
78 | 77 | adantl 482 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝑋 ∈ V) |
79 | | xpexg 6960 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V) |
80 | 78, 78, 79 | syl2anc 693 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑋 × 𝑋) ∈ V) |
81 | | isfbas2 21639 |
. . 3
⊢ ((𝑋 × 𝑋) ∈ V → (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
82 | 80, 81 | syl 17 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
83 | 17, 76, 82 | mpbir2and 957 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |