cfilucfil - Metamath Proof Explorer

	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‘𝑋)) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))

Distinct variable groups: 𝐷,𝑎 𝑋,𝑎 𝐹,𝑎,𝑥 𝑥,𝐷,𝑦 𝑥,𝐹,𝑦 𝑥,𝑋,𝑦,𝑎 𝑦,𝐷 𝐶,𝑎,𝑥,𝑦

Proof of Theorem cfilucfil Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		metust.1	. . . . 5 ⊢ 𝐹 = ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
2	1	metust 22564	. . . 4 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3		cfilufbas 22294	. . . 4 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
4	2, 3	sylan 489	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5		simpllr 817	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ (PsMet‘𝑋))
6		psmetf 22312	. . . . . 6 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
7		ffun 6209	. . . . . 6 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → Fun 𝐷)
8	5, 6, 7	3syl 18	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → Fun 𝐷)
9	2	ad2antrr 764	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10		simplr 809	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
11	1	metustfbas 22563	. . . . . . . 8 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
12	11	ad2antrr 764	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13		cnvimass 5643	. . . . . . . 8 ⊢ (^◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14		fdm 6212	. . . . . . . . 9 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → dom 𝐷 = (𝑋 × 𝑋))
15	5, 6, 14	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → dom 𝐷 = (𝑋 × 𝑋))
16	13, 15	syl5sseq 3794	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17		simpr 479	. . . . . . . . . . 11 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
18	17	rphalfcld 12077	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
19		eqidd 2761	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
20		oveq2 6821	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
21	20	imaeq2d 5624	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 / 2) → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
22	21	eqeq2d 2770	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 / 2) → ((^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2)))))
23	22	rspcev 3449	. . . . . . . . . 10 ⊢ (((𝑥 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
24	18, 19, 23	syl2anc 696	. . . . . . . . 9 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
25	1	metustel 22556	. . . . . . . . . 10 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))))
26	25	biimpar 503	. . . . . . . . 9 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
27	5, 24, 26	syl2anc 696	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
28		0xr 10278	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^*)
30		rpxr 12033	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
31		0le0 11302	. . . . . . . . . . 11 ⊢ 0 ≤ 0
32	31	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ 0)
33		rpre 12032	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
34	33	rehalfcld 11471	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
35		rphalflt 12053	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
36	34, 33, 35	ltled 10377	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ≤ 𝑥)
37		icossico 12436	. . . . . . . . . 10 ⊢ (((0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
38	29, 30, 32, 36, 37	syl22anc 1478	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
39		imass2 5659	. . . . . . . . 9 ⊢ ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
40	17, 38, 39	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
41		sseq1 3767	. . . . . . . . 9 ⊢ (𝑤 = (^◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))))
42	41	rspcev 3449	. . . . . . . 8 ⊢ (((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
43	27, 40, 42	syl2anc 696	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
44		elfg 21876	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))))
45	44	biimpar 503	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
46	12, 16, 43, 45	syl12anc 1475	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
47		cfiluexsm 22295	. . . . . 6 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ∧ (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
48	9, 10, 46, 47	syl3anc 1477	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
49		funimass2 6133	. . . . . . 7 ⊢ ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
50	49	ex 449	. . . . . 6 ⊢ (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
51	50	reximdv 3154	. . . . 5 ⊢ (Fun 𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
52	8, 48, 51	sylc 65	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
53	52	ralrimiva 3104	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
54	4, 53	jca 555	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
55		simprl 811	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
56		oveq2 6821	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
57	56	sseq2d 3774	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
58	57	rexbidv 3190	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
59		simp-4r 827	. . . . . . . . 9 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
60	59	simprd 482	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
61		simplr 809	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ⁺)
62	58, 60, 61	rspcdva 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[,)𝑥)
67	65, 66	nfral 3083	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
68	64, 67	nfan 1977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
69	63, 68	nfan 1977	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
70		nfv 1992	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
71	69, 70	nfan 1977	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
72		nfv 1992	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑎 ∈ ℝ⁺
73	71, 72	nfan 1977	. . . . . . . . 9 ⊢ Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺)
74		nfv 1992	. . . . . . . . 9 ⊢ Ⅎ𝑦(^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣
75	73, 74	nfan 1977	. . . . . . . 8 ⊢ Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
76	55	ad4antr 771	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋))
77		fbelss 21838	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
78	76, 77	sylancom 704	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
79		xpss12 5281	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
80	78, 78, 79	syl2anc 696	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
81		simp-6r 835	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋))
82	81, 6, 14	3syl 18	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋))
83	80, 82	sseqtr4d 3783	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
84	83	ex 449	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
85	75, 84	ralrimi 3095	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
86		r19.29r 3211	. . . . . . . 8 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
87		sseqin2 3960	. . . . . . . . . . . . 13 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
88	87	biimpi 206	. . . . . . . . . . . 12 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
89	88	adantl 473	. . . . . . . . . . 11 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
90		dminss 5705	. . . . . . . . . . 11 ⊢ (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
91	89, 90	syl6eqssr 3797	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
92		imass2 5659	. . . . . . . . . . 11 ⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
93	92	adantr 472	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
94	91, 93	sstrd 3754	. . . . . . . . 9 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
95	94	reximi 3149	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
96	86, 95	syl 17	. . . . . . 7 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
97	62, 85, 96	syl2anc 696	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
98		r19.41v 3227	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
99		sstr 3752	. . . . . . . 8 ⊢ (((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
100	99	reximi 3149	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
101	98, 100	sylbir 225	. . . . . 6 ⊢ ((∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
102	97, 101	sylancom 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𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹)
105	1	metustel 22556	. . . . . . . . 9 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎))))
106	105	biimpa 502	. . . . . . . 8 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
107	103, 104, 106	syl2anc 696	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
108		r19.41v 3227	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣))
109		sseq1 3767	. . . . . . . . . 10 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
110	109	biimpa 502	. . . . . . . . 9 ⊢ ((𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
111	110	reximi 3149	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
112	108, 111	sylbir 225	. . . . . . 7 ⊢ ((∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
113	107, 112	sylancom 704	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
114	11	ad2antrr 764	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
115		elfg 21876	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)))
116	115	biimpa 502	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
117	114, 116	sylancom 704	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
118	117	simprd 482	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
119	113, 118	r19.29a 3216	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
120	102, 119	r19.29a 3216	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
121	120	ralrimiva 3104	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
122	2	adantr 472	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
123		iscfilu 22293	. . . 4 ⊢ (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
124	122, 123	syl 17	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
125	55, 121, 124	mpbir2and 995	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
126	54, 125	impbida 913	1 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)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 CauFil_uccfilu 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

W3C validator