| Step | Hyp | Ref
| Expression |
| 1 | | metust.1 |
. . . . 5
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
| 2 | 1 | metust 24571 |
. . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
| 3 | | cfilufbas 24298 |
. . . 4
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
| 4 | 2, 3 | sylan 580 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋)) |
| 5 | | simpllr 776 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋)) |
| 6 | | psmetf 24316 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 7 | | ffun 6739 |
. . . . . 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 24570 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
| 12 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
| 13 | | cnvimass 6100 |
. . . . . . . 8
⊢ (◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷 |
| 14 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
| 15 | 5, 6, 14 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋)) |
| 16 | 13, 15 | sseqtrid 4026 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋)) |
| 17 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
| 18 | 17 | rphalfcld 13089 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
| 19 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
| 20 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2))) |
| 21 | 20 | imaeq2d 6078 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 / 2) → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)(𝑥 / 2)))) |
| 22 | 21 | rspceeqv 3645 |
. . . . . . . . . 10
⊢ (((𝑥 / 2) ∈ ℝ+
∧ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
| 23 | 18, 19, 22 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑎 ∈
ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) |
| 24 | 1 | metustel 24563 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎)))) |
| 25 | 24 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ+
(◡𝐷 “ (0[,)(𝑥 / 2))) = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
| 26 | 5, 23, 25 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹) |
| 27 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ∈ ℝ*) |
| 29 | | rpxr 13044 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
| 30 | | 0le0 12367 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
| 31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 0) |
| 32 | | rpre 13043 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 33 | 32 | rehalfcld 12513 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
| 34 | | rphalflt 13064 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) < 𝑥) |
| 35 | 33, 32, 34 | ltled 11409 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ≤ 𝑥) |
| 36 | | icossico 13457 |
. . . . . . . . . 10
⊢ (((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) ∧ (0 ≤ 0
∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥)) |
| 37 | 28, 29, 31, 35, 36 | syl22anc 839 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (0[,)(𝑥 / 2))
⊆ (0[,)𝑥)) |
| 38 | | imass2 6120 |
. . . . . . . . 9
⊢
((0[,)(𝑥 / 2))
⊆ (0[,)𝑥) →
(◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 39 | 17, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 40 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑤 = (◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)) ↔ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥)))) |
| 41 | 40 | rspcev 3622 |
. . . . . . . 8
⊢ (((◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 42 | 26, 39, 41 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 43 | | elfg 23879 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥))))) |
| 44 | 43 | biimpar 477 |
. . . . . . 7
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (◡𝐷 “ (0[,)𝑥)))) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
| 45 | 12, 16, 42, 44 | syl12anc 837 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) |
| 46 | | cfiluexsm 24299 |
. . . . . 6
⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ∧ (◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 47 | 9, 10, 45, 46 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) |
| 48 | | funimass2 6649 |
. . . . . . 7
⊢ ((Fun
𝐷 ∧ (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
| 49 | 48 | ex 412 |
. . . . . 6
⊢ (Fun
𝐷 → ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
| 50 | 49 | reximdv 3170 |
. . . . 5
⊢ (Fun
𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
| 51 | 8, 47, 50 | sylc 65 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
| 52 | 51 | ralrimiva 3146 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
| 53 | 4, 52 | jca 511 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
| 54 | | simprl 771 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋)) |
| 55 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎)) |
| 56 | 55 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
| 57 | 56 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))) |
| 58 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
| 59 | 58 | simprd 495 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
| 60 | | simplr 769 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ+) |
| 61 | 57, 59, 60 | rspcdva 3623 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)) |
| 62 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) |
| 63 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋) |
| 64 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ+ |
| 65 | | nfre1 3285 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
| 66 | 64, 65 | nfralw 3311 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) |
| 67 | 63, 66 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
| 68 | 62, 67 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
| 69 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) |
| 70 | 68, 69 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) |
| 71 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑎 ∈
ℝ+ |
| 72 | 70, 71 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) |
| 73 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦(◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣 |
| 74 | 72, 73 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 75 | 54 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋)) |
| 76 | | fbelss 23841 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
| 77 | 75, 76 | sylancom 588 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋) |
| 78 | | xpss12 5700 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
| 79 | 77, 77, 78 | syl2anc 584 |
. . . . . . . . . 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 4021 |
. . . . . . . . 9
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷) |
| 83 | 82 | ex 412 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷)) |
| 84 | 74, 83 | ralrimi 3257 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) |
| 85 | | r19.29r 3116 |
. . . . . . . 8
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷)) |
| 86 | | sseqin2 4223 |
. . . . . . . . . . . . 13
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
| 87 | 86 | biimpi 216 |
. . . . . . . . . . . 12
⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
| 88 | 87 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦)) |
| 89 | | dminss 6173 |
. . . . . . . . . . 11
⊢ (dom
𝐷 ∩ (𝑦 × 𝑦)) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) |
| 90 | 88, 89 | eqsstrrdi 4029 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))) |
| 91 | | imass2 6120 |
. . . . . . . . . . 11
⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 92 | 91 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 93 | 90, 92 | sstrd 3994 |
. . . . . . . . 9
⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 94 | 93 | reximi 3084 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 95 | 85, 94 | syl 17 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 96 | 61, 84, 95 | syl2anc 584 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎))) |
| 97 | | r19.41v 3189 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
| 98 | | sstr 3992 |
. . . . . . . 8
⊢ (((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣) |
| 99 | 98 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 ((𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
| 100 | 97, 99 | sylbir 235 |
. . . . . 6
⊢
((∃𝑦 ∈
𝐶 (𝑦 × 𝑦) ⊆ (◡𝐷 “ (0[,)𝑎)) ∧ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
| 101 | 96, 100 | sylancom 588 |
. . . . 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 24563 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)))) |
| 105 | 104 | biimpa 476 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
| 106 | 102, 103,
105 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎))) |
| 107 | | r19.41v 3189 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣)) |
| 108 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑤 = (◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)) |
| 109 | 108 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝑤 = (◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 110 | 109 | reximi 3084 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ+ (𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 111 | 107, 110 | sylbir 235 |
. . . . . . 7
⊢
((∃𝑎 ∈
ℝ+ 𝑤 =
(◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 112 | 106, 111 | sylancom 588 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 113 | 11 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) |
| 114 | | elfg 23879 |
. . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))) |
| 115 | 114 | biimpa 476 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
| 116 | 113, 115 | sylancom 588 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
| 117 | 116 | simprd 495 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) |
| 118 | 112, 117 | r19.29a 3162 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ+ (◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) |
| 119 | 101, 118 | r19.29a 3162 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
| 120 | 119 | ralrimiva 3146 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣) |
| 121 | 2 | adantr 480 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) |
| 122 | | iscfilu 24297 |
. . . 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[,)𝑥)))) |