Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . 5
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
2 | 1 | metust 22363 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
3 | | cfilufbas 22093 |
. . . 4
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
4 | 2, 3 | sylan 488 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
5 | | simpllr 799 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
6 | | psmetf 22111 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
7 | | ffun 6048 |
. . . . . 6
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun
𝐷) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → Fun 𝐷) |
9 | 2 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
10 | | simplr 792 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
(CauFilu‘((𝑋 × 𝑋)filGen𝐹))) |
11 | 1 | metustfbas 22362 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
12 | 11 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
13 | | cnvimass 5485 |
. . . . . . . 8
⊢ (◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷 |
14 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
15 | 5, 6, 14 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
16 | 13, 15 | syl5sseq 3653 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋)) |
17 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
18 | 17 | rphalfcld 11884 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
19 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
20 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2))) |
21 | 20 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 / 2) → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
22 | 21 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 / 2) → ((◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎)) ↔ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2))))) |
23 | 22 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑥 / 2) ∈ ℝ+
∧ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
24 | 18, 19, 23 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈
ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
25 | 1 | metustel 22355 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎)))) |
26 | 25 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ+
(◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
27 | 5, 24, 26 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
28 | | 0xr 10086 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ∈ ℝ*) |
30 | | rpxr 11840 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
31 | | 0le0 11110 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 0) |
33 | | rpre 11839 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
34 | 33 | rehalfcld 11279 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
35 | | rphalflt 11860 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) < 𝑥) |
36 | 34, 33, 35 | ltled 10185 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ≤ 𝑥) |
37 | | icossico 12243 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) ∧ (0 ≤ 0
∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥)) |
38 | 29, 30, 32, 36, 37 | syl22anc 1327 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (0[,)(𝑥 / 2))
⊆ (0[,)𝑥)) |
39 | | imass2 5501 |
. . . . . . . . 9
⊢
((0[,)(𝑥 / 2))
⊆ (0[,)𝑥) →
(◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
40 | 17, 38, 39 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
41 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑤 = (◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)) ↔ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥)))) |
42 | 41 | rspcev 3309 |
. . . . . . . 8
⊢ (((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
43 | 27, 40, 42 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
44 | | elfg 21675 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))))) |
45 | 44 | biimpar 502 |
. . . . . . 7
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)))) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
46 | 12, 16, 43, 45 | syl12anc 1324 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
47 | | cfiluexsm 22094 |
. . . . . 6
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ∧ (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
48 | 9, 10, 46, 47 | syl3anc 1326 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
49 | | funimass2 5972 |
. . . . . . 7
⊢ ((Fun
𝐷 ∧ (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
50 | 49 | ex 450 |
. . . . . 6
⊢ (Fun
𝐷 → ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
51 | 50 | reximdv 3016 |
. . . . 5
⊢ (Fun
𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
52 | 8, 48, 51 | sylc 65 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
53 | 52 | ralrimiva 2966 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
54 | 4, 53 | jca 554 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
55 | | simprl 794 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋)) |
56 | | simp-4r 807 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
57 | 56 | simprd 479 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
58 | | simplr 792 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ+) |
59 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎)) |
60 | 59 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
61 | 60 | rexbidv 3052 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
62 | 61 | rspccv 3306 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) → (𝑎 ∈ ℝ+ →
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
63 | 57, 58, 62 | sylc 65 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)) |
64 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) |
65 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋) |
66 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ+ |
67 | | nfre1 3005 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
68 | 66, 67 | nfral 2945 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
69 | 65, 68 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
70 | 64, 69 | nfan 1828 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
71 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) |
72 | 70, 71 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) |
73 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑎 ∈
ℝ+ |
74 | 72, 73 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) |
75 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑦(◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣 |
76 | 74, 75 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
77 | 55 | ad4antr 768 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋)) |
78 | | fbelss 21637 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
79 | 77, 78 | sylancom 701 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
80 | | xpss12 5225 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
81 | 79, 79, 80 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
82 | | simp-6r 811 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋)) |
83 | 82, 6, 14 | 3syl 18 |
. . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋)) |
84 | 81, 83 | sseqtr4d 3642 |
. . . . . . . . 9
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷) |
85 | 84 | ex 450 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷)) |
86 | 76, 85 | ralrimi 2957 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) |
87 | | r19.29r 3073 |
. . . . . . . 8
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷)) |
88 | | sseqin2 3817 |
. . . . . . . . . . . . 13
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
89 | 88 | biimpi 206 |
. . . . . . . . . . . 12
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
90 | 89 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
91 | | dminss 5547 |
. . . . . . . . . . 11
⊢ (dom
𝐷 ∩ (𝑦 × 𝑦)) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) |
92 | 90, 91 | syl6eqssr 3656 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))) |
93 | | imass2 5501 |
. . . . . . . . . . 11
⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
94 | 93 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
95 | 92, 94 | sstrd 3613 |
. . . . . . . . 9
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
96 | 95 | reximi 3011 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
97 | 87, 96 | syl 17 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
98 | 63, 86, 97 | syl2anc 693 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
99 | | r19.41v 3089 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
100 | | sstr 3611 |
. . . . . . . 8
⊢ (((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣) |
101 | 100 | reximi 3011 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
102 | 99, 101 | sylbir 225 |
. . . . . 6
⊢
((∃𝑦 ∈
𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
103 | 98, 102 | sylancom 701 |
. . . . 5
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
104 | | simp-5r 809 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝐷 ∈ (PsMet‘𝑋)) |
105 | | simplr 792 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹) |
106 | 1 | metustel 22355 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)))) |
107 | 106 | biimpa 501 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
108 | 104, 105,
107 | syl2anc 693 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
109 | | r19.41v 3089 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣)) |
110 | | sseq1 3626 |
. . . . . . . . . 10
⊢ (𝑤 = (◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
111 | 110 | biimpa 501 |
. . . . . . . . 9
⊢ ((𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
112 | 111 | reximi 3011 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
113 | 109, 112 | sylbir 225 |
. . . . . . 7
⊢
((∃𝑎 ∈
ℝ+ 𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
114 | 108, 113 | sylancom 701 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
115 | 11 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
116 | | elfg 21675 |
. . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))) |
117 | 116 | biimpa 501 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
118 | 115, 117 | sylancom 701 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
119 | 118 | simprd 479 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) |
120 | 114, 119 | r19.29a 3078 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
121 | 103, 120 | r19.29a 3078 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
122 | 121 | ralrimiva 2966 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
123 | 2 | adantr 481 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
124 | | iscfilu 22092 |
. . . 4
⊢ (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣))) |
125 | 123, 124 | syl 17 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣))) |
126 | 55, 122, 125 | mpbir2and 957 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) |
127 | 54, 126 | impbida 877 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |