Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . 5
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
2 | 1 | metust 23323 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
3 | | cfilufbas 23053 |
. . . 4
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
4 | 2, 3 | sylan 583 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
5 | | simpllr 776 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
6 | | psmetf 23071 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
7 | | ffun 6517 |
. . . . . 6
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun
𝐷) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → Fun 𝐷) |
9 | 2 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
10 | | simplr 769 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
(CauFilu‘((𝑋 × 𝑋)filGen𝐹))) |
11 | 1 | metustfbas 23322 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
12 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
13 | | cnvimass 5933 |
. . . . . . . 8
⊢ (◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷 |
14 | | fdm 6523 |
. . . . . . . . 9
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
15 | 5, 6, 14 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
16 | 13, 15 | sseqtrid 3939 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋)) |
17 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
18 | 17 | rphalfcld 12538 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
19 | | eqidd 2740 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
20 | | oveq2 7190 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2))) |
21 | 20 | imaeq2d 5913 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 / 2) → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
22 | 21 | rspceeqv 3544 |
. . . . . . . . . 10
⊢ (((𝑥 / 2) ∈ ℝ+
∧ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
23 | 18, 19, 22 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈
ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
24 | 1 | metustel 23315 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎)))) |
25 | 24 | biimpar 481 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ+
(◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
26 | 5, 23, 25 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
27 | | 0xr 10778 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ∈ ℝ*) |
29 | | rpxr 12493 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
30 | | 0le0 11829 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 0) |
32 | | rpre 12492 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
33 | 32 | rehalfcld 11975 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
34 | | rphalflt 12513 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) < 𝑥) |
35 | 33, 32, 34 | ltled 10878 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ≤ 𝑥) |
36 | | icossico 12903 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) ∧ (0 ≤ 0
∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥)) |
37 | 28, 29, 31, 35, 36 | syl22anc 838 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (0[,)(𝑥 / 2))
⊆ (0[,)𝑥)) |
38 | | imass2 5949 |
. . . . . . . . 9
⊢
((0[,)(𝑥 / 2))
⊆ (0[,)𝑥) →
(◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
39 | 17, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
40 | | sseq1 3912 |
. . . . . . . . 9
⊢ (𝑤 = (◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)) ↔ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥)))) |
41 | 40 | rspcev 3529 |
. . . . . . . 8
⊢ (((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
42 | 26, 39, 41 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
43 | | elfg 22634 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))))) |
44 | 43 | biimpar 481 |
. . . . . . 7
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)))) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
45 | 12, 16, 42, 44 | syl12anc 836 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
46 | | cfiluexsm 23054 |
. . . . . 6
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ∧ (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
47 | 9, 10, 45, 46 | syl3anc 1372 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
48 | | funimass2 6432 |
. . . . . . 7
⊢ ((Fun
𝐷 ∧ (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
49 | 48 | ex 416 |
. . . . . 6
⊢ (Fun
𝐷 → ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
50 | 49 | reximdv 3184 |
. . . . 5
⊢ (Fun
𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
51 | 8, 47, 50 | sylc 65 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
52 | 51 | ralrimiva 3097 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
53 | 4, 52 | jca 515 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
54 | | simprl 771 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋)) |
55 | | oveq2 7190 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎)) |
56 | 55 | sseq2d 3919 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
57 | 56 | rexbidv 3208 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
58 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
59 | 58 | simprd 499 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
60 | | simplr 769 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ+) |
61 | 57, 59, 60 | rspcdva 3531 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)) |
62 | | nfv 1921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) |
63 | | nfv 1921 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋) |
64 | | nfcv 2900 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ+ |
65 | | nfre1 3217 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
66 | 64, 65 | nfralw 3139 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
67 | 63, 66 | nfan 1906 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
68 | 62, 67 | nfan 1906 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
69 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) |
70 | 68, 69 | nfan 1906 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) |
71 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑎 ∈
ℝ+ |
72 | 70, 71 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) |
73 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑦(◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣 |
74 | 72, 73 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
75 | 54 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋)) |
76 | | fbelss 22596 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
77 | 75, 76 | sylancom 591 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
78 | | xpss12 5550 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
79 | 77, 77, 78 | syl2anc 587 |
. . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
80 | | simp-6r 788 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋)) |
81 | 80, 6, 14 | 3syl 18 |
. . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋)) |
82 | 79, 81 | sseqtrrd 3928 |
. . . . . . . . 9
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷) |
83 | 82 | ex 416 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷)) |
84 | 74, 83 | ralrimi 3129 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) |
85 | | r19.29r 3169 |
. . . . . . . 8
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷)) |
86 | | sseqin2 4116 |
. . . . . . . . . . . . 13
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
87 | 86 | biimpi 219 |
. . . . . . . . . . . 12
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
88 | 87 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
89 | | dminss 5995 |
. . . . . . . . . . 11
⊢ (dom
𝐷 ∩ (𝑦 × 𝑦)) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) |
90 | 88, 89 | eqsstrrdi 3942 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))) |
91 | | imass2 5949 |
. . . . . . . . . . 11
⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
92 | 91 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
93 | 90, 92 | sstrd 3897 |
. . . . . . . . 9
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
94 | 93 | reximi 3158 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
95 | 85, 94 | syl 17 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
96 | 61, 84, 95 | syl2anc 587 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
97 | | r19.41v 3252 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
98 | | sstr 3895 |
. . . . . . . 8
⊢ (((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣) |
99 | 98 | reximi 3158 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
100 | 97, 99 | sylbir 238 |
. . . . . 6
⊢
((∃𝑦 ∈
𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
101 | 96, 100 | sylancom 591 |
. . . . 5
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
102 | | simp-5r 786 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝐷 ∈ (PsMet‘𝑋)) |
103 | | simplr 769 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹) |
104 | 1 | metustel 23315 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)))) |
105 | 104 | biimpa 480 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
106 | 102, 103,
105 | syl2anc 587 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
107 | | r19.41v 3252 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣)) |
108 | | sseq1 3912 |
. . . . . . . . . 10
⊢ (𝑤 = (◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
109 | 108 | biimpa 480 |
. . . . . . . . 9
⊢ ((𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
110 | 109 | reximi 3158 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
111 | 107, 110 | sylbir 238 |
. . . . . . 7
⊢
((∃𝑎 ∈
ℝ+ 𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
112 | 106, 111 | sylancom 591 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
113 | 11 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
114 | | elfg 22634 |
. . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))) |
115 | 114 | biimpa 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
116 | 113, 115 | sylancom 591 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
117 | 116 | simprd 499 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) |
118 | 112, 117 | r19.29a 3200 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
119 | 101, 118 | r19.29a 3200 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
120 | 119 | ralrimiva 3097 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
121 | 2 | adantr 484 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
122 | | iscfilu 23052 |
. . . 4
⊢ (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣))) |
123 | 121, 122 | syl 17 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣))) |
124 | 54, 120, 123 | mpbir2and 713 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) |
125 | 53, 124 | impbida 801 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |