Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
2 | 1 | metustel 22165 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎)))) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
4 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡𝐷 “ (0[,)𝑎)) ⊆ dom 𝐷 |
5 | | psmetf 21921 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
6 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → dom 𝐷 = (𝑋 × 𝑋)) |
9 | 4, 8 | syl5sseq 3616 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)𝑎)) ⊆ (𝑋 × 𝑋)) |
10 | 3, 9 | eqsstrd 3602 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 = (◡𝐷 “ (0[,)𝑎))) → 𝑥 ⊆ (𝑋 × 𝑋)) |
11 | 10 | ex 449 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 = (◡𝐷 “ (0[,)𝑎)) → 𝑥 ⊆ (𝑋 × 𝑋))) |
12 | 11 | rexlimdvw 3016 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎)) → 𝑥 ⊆ (𝑋 × 𝑋))) |
13 | 2, 12 | sylbid 229 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ⊆ (𝑋 × 𝑋))) |
14 | 13 | ralrimiv 2948 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝐹 𝑥 ⊆ (𝑋 × 𝑋)) |
15 | | pwssb 4548 |
. . . 4
⊢ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∀𝑥 ∈ 𝐹 𝑥 ⊆ (𝑋 × 𝑋)) |
16 | 14, 15 | sylibr 223 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐹 ⊆ 𝒫 (𝑋 × 𝑋)) |
17 | 16 | adantl 481 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ⊆ 𝒫 (𝑋 × 𝑋)) |
18 | | cnvexg 7005 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → ◡𝐷 ∈ V) |
19 | | imaexg 6995 |
. . . . . . 7
⊢ (◡𝐷 ∈ V → (◡𝐷 “ (0[,)1)) ∈ V) |
20 | | elisset 3188 |
. . . . . . 7
⊢ ((◡𝐷 “ (0[,)1)) ∈ V →
∃𝑥 𝑥 = (◡𝐷 “ (0[,)1))) |
21 | | 1rp 11712 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
22 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → (0[,)𝑎) = (0[,)1)) |
23 | 22 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)1))) |
24 | 23 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (𝑥 = (◡𝐷 “ (0[,)𝑎)) ↔ 𝑥 = (◡𝐷 “ (0[,)1)))) |
25 | 24 | rspcev 3282 |
. . . . . . . . 9
⊢ ((1
∈ ℝ+ ∧ 𝑥 = (◡𝐷 “ (0[,)1))) → ∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎))) |
26 | 21, 25 | mpan 702 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐷 “ (0[,)1)) → ∃𝑎 ∈ ℝ+
𝑥 = (◡𝐷 “ (0[,)𝑎))) |
27 | 26 | eximi 1752 |
. . . . . . 7
⊢
(∃𝑥 𝑥 = (◡𝐷 “ (0[,)1)) → ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
28 | 18, 19, 20, 27 | 4syl 19 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎))) |
29 | 2 | exbidv 1837 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (∃𝑥 𝑥 ∈ 𝐹 ↔ ∃𝑥∃𝑎 ∈ ℝ+ 𝑥 = (◡𝐷 “ (0[,)𝑎)))) |
30 | 28, 29 | mpbird 246 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 𝑥 ∈ 𝐹) |
31 | 30 | adantl 481 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 𝑥 ∈ 𝐹) |
32 | | n0 3890 |
. . . 4
⊢ (𝐹 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐹) |
33 | 31, 32 | sylibr 223 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ≠ ∅) |
34 | 1 | metustid 22169 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝑥) |
35 | 34 | adantll 746 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝑥) |
36 | | n0 3890 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ ↔
∃𝑝 𝑝 ∈ 𝑋) |
37 | 36 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑋 ≠ ∅ →
∃𝑝 𝑝 ∈ 𝑋) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑝 𝑝 ∈ 𝑋) |
39 | | opelresi 5328 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ 𝑋 → (〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋) ↔ 𝑝 ∈ 𝑋)) |
40 | 39 | ibir 256 |
. . . . . . . . . 10
⊢ (𝑝 ∈ 𝑋 → 〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋)) |
41 | | ne0i 3880 |
. . . . . . . . . 10
⊢
(〈𝑝, 𝑝〉 ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (𝑝 ∈ 𝑋 → ( I ↾ 𝑋) ≠ ∅) |
43 | 42 | exlimiv 1845 |
. . . . . . . 8
⊢
(∃𝑝 𝑝 ∈ 𝑋 → ( I ↾ 𝑋) ≠ ∅) |
44 | 38, 43 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ( I ↾ 𝑋) ≠ ∅) |
45 | 44 | adantr 480 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ( I ↾ 𝑋) ≠ ∅) |
46 | | ssn0 3928 |
. . . . . 6
⊢ ((( I
↾ 𝑋) ⊆ 𝑥 ∧ ( I ↾ 𝑋) ≠ ∅) → 𝑥 ≠ ∅) |
47 | 35, 45, 46 | syl2anc 691 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ≠ ∅) |
48 | 47 | nelrdva 3384 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ¬ ∅ ∈
𝐹) |
49 | | df-nel 2783 |
. . . 4
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
50 | 48, 49 | sylibr 223 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∅ ∉ 𝐹) |
51 | | df-ss 3554 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∩ 𝑦) = 𝑥) |
52 | 51 | biimpi 205 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∩ 𝑦) = 𝑥) |
53 | 52 | adantl 481 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∩ 𝑦) = 𝑥) |
54 | | simplrl 796 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → 𝑥 ∈ 𝐹) |
55 | 53, 54 | eqeltrd 2688 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
56 | | sseqin2 3779 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝑥 ↔ (𝑥 ∩ 𝑦) = 𝑦) |
57 | 56 | biimpi 205 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝑥 → (𝑥 ∩ 𝑦) = 𝑦) |
58 | 57 | adantl 481 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∩ 𝑦) = 𝑦) |
59 | | simplrr 797 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ 𝐹) |
60 | 58, 59 | eqeltrd 2688 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
61 | | simplr 788 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝐷 ∈ (PsMet‘𝑋)) |
62 | | simprl 790 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝑥 ∈ 𝐹) |
63 | | simprr 792 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → 𝑦 ∈ 𝐹) |
64 | 1 | metustto 22168 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) |
65 | 61, 62, 63, 64 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) |
66 | 55, 60, 65 | mpjaodan 823 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
67 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
68 | 67 | inex1 4727 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ∈ V |
69 | 68 | pwid 4122 |
. . . . . . 7
⊢ (𝑥 ∩ 𝑦) ∈ 𝒫 (𝑥 ∩ 𝑦) |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝒫 (𝑥 ∩ 𝑦)) |
71 | 70 | elpwid 4118 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) |
72 | | sseq1 3589 |
. . . . . 6
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
73 | 72 | rspcev 3282 |
. . . . 5
⊢ (((𝑥 ∩ 𝑦) ∈ 𝐹 ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
74 | 66, 71, 73 | syl2anc 691 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
75 | 74 | ralrimivva 2954 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
76 | 33, 50, 75 | 3jca 1235 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
77 | | elfvex 6131 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V) |
78 | 77 | adantl 481 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝑋 ∈ V) |
79 | | xpexg 6858 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V) |
80 | 78, 78, 79 | syl2anc 691 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑋 × 𝑋) ∈ V) |
81 | | isfbas2 21449 |
. . 3
⊢ ((𝑋 × 𝑋) ∈ V → (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
82 | 80, 81 | syl 17 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝐹 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
83 | 17, 76, 82 | mpbir2and 959 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |