MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cfilucfil Structured version   Visualization version   GIF version

Theorem cfilucfil 22283
Description: Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 22982. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
metust.1 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
Assertion
Ref Expression
cfilucfil ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Distinct variable groups:   𝐷,𝑎   𝑋,𝑎   𝐹,𝑎,𝑥   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝑥,𝑋,𝑦,𝑎   𝑦,𝐷   𝐶,𝑎,𝑥,𝑦

Proof of Theorem cfilucfil
Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 metust.1 . . . . 5 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
21metust 22282 . . . 4 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3 cfilufbas 22012 . . . 4 ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
42, 3sylan 488 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5 simpllr 798 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋))
6 psmetf 22030 . . . . . 6 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7 ffun 6010 . . . . . 6 (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun 𝐷)
85, 6, 73syl 18 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → Fun 𝐷)
92ad2antrr 761 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10 simplr 791 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)))
111metustfbas 22281 . . . . . . . 8 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
1211ad2antrr 761 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13 cnvimass 5449 . . . . . . . 8 (𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14 fdm 6013 . . . . . . . . 9 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
155, 6, 143syl 18 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋))
1613, 15syl5sseq 3637 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17 simpr 477 . . . . . . . . . . 11 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
1817rphalfcld 11835 . . . . . . . . . 10 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
19 eqidd 2622 . . . . . . . . . 10 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2))))
20 oveq2 6618 . . . . . . . . . . . . 13 (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
2120imaeq2d 5430 . . . . . . . . . . . 12 (𝑎 = (𝑥 / 2) → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)(𝑥 / 2))))
2221eqeq2d 2631 . . . . . . . . . . 11 (𝑎 = (𝑥 / 2) → ((𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)) ↔ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2)))))
2322rspcev 3298 . . . . . . . . . 10 (((𝑥 / 2) ∈ ℝ+ ∧ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)))
2418, 19, 23syl2anc 692 . . . . . . . . 9 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)))
251metustel 22274 . . . . . . . . . 10 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎))))
2625biimpar 502 . . . . . . . . 9 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
275, 24, 26syl2anc 692 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
28 0xr 10037 . . . . . . . . . . 11 0 ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → 0 ∈ ℝ*)
30 rpxr 11791 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℝ*)
31 0le0 11061 . . . . . . . . . . 11 0 ≤ 0
3231a1i 11 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → 0 ≤ 0)
33 rpre 11790 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
3433rehalfcld 11230 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
35 rphalflt 11811 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
3634, 33, 35ltled 10136 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (𝑥 / 2) ≤ 𝑥)
37 icossico 12192 . . . . . . . . . 10 (((0 ∈ ℝ*𝑥 ∈ ℝ*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
3829, 30, 32, 36, 37syl22anc 1324 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
39 imass2 5465 . . . . . . . . 9 ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥)))
4017, 38, 393syl 18 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥)))
41 sseq1 3610 . . . . . . . . 9 (𝑤 = (𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (𝐷 “ (0[,)𝑥)) ↔ (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥))))
4241rspcev 3298 . . . . . . . 8 (((𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥))) → ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))
4327, 40, 42syl2anc 692 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))
44 elfg 21594 . . . . . . . 8 (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))))
4544biimpar 502 . . . . . . 7 ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))) → (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
4612, 16, 43, 45syl12anc 1321 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
47 cfiluexsm 22013 . . . . . 6 ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ∧ (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)))
489, 10, 46, 47syl3anc 1323 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)))
49 funimass2 5935 . . . . . . 7 ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
5049ex 450 . . . . . 6 (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
5150reximdv 3011 . . . . 5 (Fun 𝐷 → (∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
528, 48, 51sylc 65 . . . 4 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
5352ralrimiva 2961 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
544, 53jca 554 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
55 simprl 793 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
56 simp-4r 806 . . . . . . . . 9 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
5756simprd 479 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
58 simplr 791 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ+)
59 oveq2 6618 . . . . . . . . . . 11 (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
6059sseq2d 3617 . . . . . . . . . 10 (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
6160rexbidv 3046 . . . . . . . . 9 (𝑥 = 𝑎 → (∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
6261rspccv 3295 . . . . . . . 8 (∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) → (𝑎 ∈ ℝ+ → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
6357, 58, 62sylc 65 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
64 nfv 1840 . . . . . . . . . . . 12 𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
65 nfv 1840 . . . . . . . . . . . . 13 𝑦 𝐶 ∈ (fBas‘𝑋)
66 nfcv 2761 . . . . . . . . . . . . . 14 𝑦+
67 nfre1 3000 . . . . . . . . . . . . . 14 𝑦𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
6866, 67nfral 2940 . . . . . . . . . . . . 13 𝑦𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
6965, 68nfan 1825 . . . . . . . . . . . 12 𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
7064, 69nfan 1825 . . . . . . . . . . 11 𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
71 nfv 1840 . . . . . . . . . . 11 𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
7270, 71nfan 1825 . . . . . . . . . 10 𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
73 nfv 1840 . . . . . . . . . 10 𝑦 𝑎 ∈ ℝ+
7472, 73nfan 1825 . . . . . . . . 9 𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+)
75 nfv 1840 . . . . . . . . 9 𝑦(𝐷 “ (0[,)𝑎)) ⊆ 𝑣
7674, 75nfan 1825 . . . . . . . 8 𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
7755ad4antr 767 . . . . . . . . . . . 12 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝐶 ∈ (fBas‘𝑋))
78 fbelss 21556 . . . . . . . . . . . 12 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦𝐶) → 𝑦𝑋)
7977, 78sylancom 700 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝑦𝑋)
80 xpss12 5191 . . . . . . . . . . 11 ((𝑦𝑋𝑦𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
8179, 79, 80syl2anc 692 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
82 simp-6r 810 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝐷 ∈ (PsMet‘𝑋))
8382, 6, 143syl 18 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → dom 𝐷 = (𝑋 × 𝑋))
8481, 83sseqtr4d 3626 . . . . . . . . 9 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
8584ex 450 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
8676, 85ralrimi 2952 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
87 r19.29r 3067 . . . . . . . 8 ((∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
88 sseqin2 3800 . . . . . . . . . . . . 13 ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
8988biimpi 206 . . . . . . . . . . . 12 ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
9089adantl 482 . . . . . . . . . . 11 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
91 dminss 5511 . . . . . . . . . . 11 (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
9290, 91syl6eqssr 3640 . . . . . . . . . 10 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
93 imass2 5465 . . . . . . . . . . 11 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (𝐷 “ (0[,)𝑎)))
9493adantr 481 . . . . . . . . . 10 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (𝐷 “ (0[,)𝑎)))
9592, 94sstrd 3597 . . . . . . . . 9 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9695reximi 3006 . . . . . . . 8 (∃𝑦𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9787, 96syl 17 . . . . . . 7 ((∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9863, 86, 97syl2anc 692 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
99 r19.41v 3082 . . . . . . 7 (∃𝑦𝐶 ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
100 sstr 3595 . . . . . . . 8 (((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
101100reximi 3006 . . . . . . 7 (∃𝑦𝐶 ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
10299, 101sylbir 225 . . . . . 6 ((∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
10398, 102sylancom 700 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
104 simp-5r 808 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → 𝐷 ∈ (PsMet‘𝑋))
105 simplr 791 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → 𝑤𝐹)
1061metustel 22274 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → (𝑤𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎))))
107106biimpa 501 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤𝐹) → ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
108104, 105, 107syl2anc 692 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
109 r19.41v 3082 . . . . . . . 8 (∃𝑎 ∈ ℝ+ (𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) ↔ (∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣))
110 sseq1 3610 . . . . . . . . . 10 (𝑤 = (𝐷 “ (0[,)𝑎)) → (𝑤𝑣 ↔ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
111110biimpa 501 . . . . . . . . 9 ((𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
112111reximi 3006 . . . . . . . 8 (∃𝑎 ∈ ℝ+ (𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
113109, 112sylbir 225 . . . . . . 7 ((∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
114108, 113sylancom 700 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
11511ad2antrr 761 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
116 elfg 21594 . . . . . . . . 9 (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣)))
117116biimpa 501 . . . . . . . 8 ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣))
118115, 117sylancom 700 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣))
119118simprd 479 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤𝐹 𝑤𝑣)
120114, 119r19.29a 3072 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
121103, 120r19.29a 3072 . . . 4 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
122121ralrimiva 2961 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
1232adantr 481 . . . 4 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
124 iscfilu 22011 . . . 4 (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
125123, 124syl 17 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
12655, 122, 125mpbir2and 956 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)))
12754, 126impbida 876 1 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  cin 3558  wss 3559  c0 3896   class class class wbr 4618  cmpt 4678   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  Fun wfun 5846  wf 5848  cfv 5852  (class class class)co 6610  0cc0 9887  *cxr 10024  cle 10026   / cdiv 10635  2c2 11021  +crp 11783  [,)cico 12126  PsMetcpsmet 19658  fBascfbas 19662  filGencfg 19663  UnifOncust 21922  CauFiluccfilu 22009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-2 11030  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ico 12130  df-psmet 19666  df-fbas 19671  df-fg 19672  df-fil 21569  df-ust 21923  df-cfilu 22010
This theorem is referenced by:  cfilucfil2  22285
  Copyright terms: Public domain W3C validator