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

Theorem cfilucfil 22565
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 23263. (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 22564 . . . 4 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3 cfilufbas 22294 . . . 4 ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
42, 3sylan 489 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5 simpllr 817 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (PsMet‘𝑋))
6 psmetf 22312 . . . . . 6 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7 ffun 6209 . . . . . 6 (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun 𝐷)
85, 6, 73syl 18 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → Fun 𝐷)
92ad2antrr 764 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10 simplr 809 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)))
111metustfbas 22563 . . . . . . . 8 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
1211ad2antrr 764 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13 cnvimass 5643 . . . . . . . 8 (𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14 fdm 6212 . . . . . . . . 9 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
155, 6, 143syl 18 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → dom 𝐷 = (𝑋 × 𝑋))
1613, 15syl5sseq 3794 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17 simpr 479 . . . . . . . . . . 11 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
1817rphalfcld 12077 . . . . . . . . . 10 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
19 eqidd 2761 . . . . . . . . . 10 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2))))
20 oveq2 6821 . . . . . . . . . . . . 13 (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
2120imaeq2d 5624 . . . . . . . . . . . 12 (𝑎 = (𝑥 / 2) → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)(𝑥 / 2))))
2221eqeq2d 2770 . . . . . . . . . . 11 (𝑎 = (𝑥 / 2) → ((𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)) ↔ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2)))))
2322rspcev 3449 . . . . . . . . . 10 (((𝑥 / 2) ∈ ℝ+ ∧ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)))
2418, 19, 23syl2anc 696 . . . . . . . . 9 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎)))
251metustel 22556 . . . . . . . . . 10 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎))))
2625biimpar 503 . . . . . . . . 9 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)(𝑥 / 2))) = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
275, 24, 26syl2anc 696 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
28 0xr 10278 . . . . . . . . . . 11 0 ∈ ℝ*
2928a1i 11 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → 0 ∈ ℝ*)
30 rpxr 12033 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℝ*)
31 0le0 11302 . . . . . . . . . . 11 0 ≤ 0
3231a1i 11 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → 0 ≤ 0)
33 rpre 12032 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
3433rehalfcld 11471 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
35 rphalflt 12053 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
3634, 33, 35ltled 10377 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (𝑥 / 2) ≤ 𝑥)
37 icossico 12436 . . . . . . . . . 10 (((0 ∈ ℝ*𝑥 ∈ ℝ*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
3829, 30, 32, 36, 37syl22anc 1478 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
39 imass2 5659 . . . . . . . . 9 ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥)))
4017, 38, 393syl 18 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥)))
41 sseq1 3767 . . . . . . . . 9 (𝑤 = (𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (𝐷 “ (0[,)𝑥)) ↔ (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥))))
4241rspcev 3449 . . . . . . . 8 (((𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (𝐷 “ (0[,)(𝑥 / 2))) ⊆ (𝐷 “ (0[,)𝑥))) → ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))
4327, 40, 42syl2anc 696 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))
44 elfg 21876 . . . . . . . 8 (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))))
4544biimpar 503 . . . . . . 7 ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤 ⊆ (𝐷 “ (0[,)𝑥)))) → (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
4612, 16, 43, 45syl12anc 1475 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
47 cfiluexsm 22295 . . . . . 6 ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ∧ (𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)))
489, 10, 46, 47syl3anc 1477 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)))
49 funimass2 6133 . . . . . . 7 ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
5049ex 449 . . . . . 6 (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
5150reximdv 3154 . . . . 5 (Fun 𝐷 → (∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑥)) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
528, 48, 51sylc 65 . . . 4 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ+) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
5352ralrimiva 3104 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
544, 53jca 555 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
55 simprl 811 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
56 oveq2 6821 . . . . . . . . . 10 (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
5756sseq2d 3774 . . . . . . . . 9 (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
5857rexbidv 3190 . . . . . . . 8 (𝑥 = 𝑎 → (∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
59 simp-4r 827 . . . . . . . . 9 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
6059simprd 482 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
61 simplr 809 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ+)
6258, 60, 61rspcdva 3455 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
63 nfv 1992 . . . . . . . . . . . 12 𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
64 nfv 1992 . . . . . . . . . . . . 13 𝑦 𝐶 ∈ (fBas‘𝑋)
65 nfcv 2902 . . . . . . . . . . . . . 14 𝑦+
66 nfre1 3143 . . . . . . . . . . . . . 14 𝑦𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
6765, 66nfral 3083 . . . . . . . . . . . . 13 𝑦𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
6864, 67nfan 1977 . . . . . . . . . . . 12 𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
6963, 68nfan 1977 . . . . . . . . . . 11 𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
70 nfv 1992 . . . . . . . . . . 11 𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
7169, 70nfan 1977 . . . . . . . . . 10 𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
72 nfv 1992 . . . . . . . . . 10 𝑦 𝑎 ∈ ℝ+
7371, 72nfan 1977 . . . . . . . . 9 𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+)
74 nfv 1992 . . . . . . . . 9 𝑦(𝐷 “ (0[,)𝑎)) ⊆ 𝑣
7573, 74nfan 1977 . . . . . . . 8 𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
7655ad4antr 771 . . . . . . . . . . . 12 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝐶 ∈ (fBas‘𝑋))
77 fbelss 21838 . . . . . . . . . . . 12 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦𝐶) → 𝑦𝑋)
7876, 77sylancom 704 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝑦𝑋)
79 xpss12 5281 . . . . . . . . . . 11 ((𝑦𝑋𝑦𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
8078, 78, 79syl2anc 696 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
81 simp-6r 835 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → 𝐷 ∈ (PsMet‘𝑋))
8281, 6, 143syl 18 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → dom 𝐷 = (𝑋 × 𝑋))
8380, 82sseqtr4d 3783 . . . . . . . . 9 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
8483ex 449 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
8575, 84ralrimi 3095 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
86 r19.29r 3211 . . . . . . . 8 ((∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
87 sseqin2 3960 . . . . . . . . . . . . 13 ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
8887biimpi 206 . . . . . . . . . . . 12 ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
8988adantl 473 . . . . . . . . . . 11 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
90 dminss 5705 . . . . . . . . . . 11 (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
9189, 90syl6eqssr 3797 . . . . . . . . . 10 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
92 imass2 5659 . . . . . . . . . . 11 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (𝐷 “ (0[,)𝑎)))
9392adantr 472 . . . . . . . . . 10 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (𝐷 “ (0[,)𝑎)))
9491, 93sstrd 3754 . . . . . . . . 9 (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9594reximi 3149 . . . . . . . 8 (∃𝑦𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9686, 95syl 17 . . . . . . 7 ((∃𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
9762, 85, 96syl2anc 696 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)))
98 r19.41v 3227 . . . . . . 7 (∃𝑦𝐶 ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
99 sstr 3752 . . . . . . . 8 (((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
10099reximi 3149 . . . . . . 7 (∃𝑦𝐶 ((𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
10198, 100sylbir 225 . . . . . 6 ((∃𝑦𝐶 (𝑦 × 𝑦) ⊆ (𝐷 “ (0[,)𝑎)) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
10297, 101sylancom 704 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ+) ∧ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
103 simp-5r 831 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → 𝐷 ∈ (PsMet‘𝑋))
104 simplr 809 . . . . . . . 8 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → 𝑤𝐹)
1051metustel 22556 . . . . . . . . 9 (𝐷 ∈ (PsMet‘𝑋) → (𝑤𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎))))
106105biimpa 502 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤𝐹) → ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
107103, 104, 106syl2anc 696 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)))
108 r19.41v 3227 . . . . . . . 8 (∃𝑎 ∈ ℝ+ (𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) ↔ (∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣))
109 sseq1 3767 . . . . . . . . . 10 (𝑤 = (𝐷 “ (0[,)𝑎)) → (𝑤𝑣 ↔ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
110109biimpa 502 . . . . . . . . 9 ((𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
111110reximi 3149 . . . . . . . 8 (∃𝑎 ∈ ℝ+ (𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
112108, 111sylbir 225 . . . . . . 7 ((∃𝑎 ∈ ℝ+ 𝑤 = (𝐷 “ (0[,)𝑎)) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
113107, 112sylancom 704 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤𝐹) ∧ 𝑤𝑣) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
11411ad2antrr 764 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
115 elfg 21876 . . . . . . . . 9 (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣)))
116115biimpa 502 . . . . . . . 8 ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣))
117114, 116sylancom 704 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤𝐹 𝑤𝑣))
118117simprd 482 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤𝐹 𝑤𝑣)
119113, 118r19.29a 3216 . . . . 5 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ+ (𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
120102, 119r19.29a 3216 . . . 4 ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
121120ralrimiva 3104 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
1222adantr 472 . . . 4 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
123 iscfilu 22293 . . . 4 (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
124122, 123syl 17 . . 3 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
12555, 121, 124mpbir2and 995 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)))
12654, 125impbida 913 1 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  cin 3714  wss 3715  c0 4058   class class class wbr 4804  cmpt 4881   × cxp 5264  ccnv 5265  dom cdm 5266  ran crn 5267  cima 5269  Fun wfun 6043  wf 6045  cfv 6049  (class class class)co 6813  0cc0 10128  *cxr 10265  cle 10267   / cdiv 10876  2c2 11262  +crp 12025  [,)cico 12370  PsMetcpsmet 19932  fBascfbas 19936  filGencfg 19937  UnifOncust 22204  CauFiluccfilu 22291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-2 11271  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ico 12374  df-psmet 19940  df-fbas 19945  df-fg 19946  df-fil 21851  df-ust 22205  df-cfilu 22292
This theorem is referenced by:  cfilucfil2  22567
  Copyright terms: Public domain W3C validator