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 24480

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 25198. (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 24479	. . . 4 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3		cfilufbas 24209	. . . 4 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
4	2, 3	sylan 580	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5		simpllr 775	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ (PsMet‘𝑋))
6		psmetf 24227	. . . . . 6 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
7		ffun 6673	. . . . . 6 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → Fun 𝐷)
8	5, 6, 7	3syl 18	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → Fun 𝐷)
9	2	ad2antrr 726	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10		simplr 768	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
11	1	metustfbas 24478	. . . . . . . 8 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
12	11	ad2antrr 726	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13		cnvimass 6042	. . . . . . . 8 ⊢ (^◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14		fdm 6679	. . . . . . . . 9 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → dom 𝐷 = (𝑋 × 𝑋))
15	5, 6, 14	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → dom 𝐷 = (𝑋 × 𝑋))
16	13, 15	sseqtrid 3986	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
18	17	rphalfcld 12983	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
19		eqidd 2730	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
20		oveq2 7377	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
21	20	imaeq2d 6020	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 / 2) → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
22	21	rspceeqv 3608	. . . . . . . . . 10 ⊢ (((𝑥 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
23	18, 19, 22	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
24	1	metustel 24471	. . . . . . . . . 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‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
27		0xr 11197	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^*)
29		rpxr 12937	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
30		0le0 12263	. . . . . . . . . . 11 ⊢ 0 ≤ 0
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ 0)
32		rpre 12936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
33	32	rehalfcld 12405	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
34		rphalflt 12958	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
35	33, 32, 34	ltled 11298	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ≤ 𝑥)
36		icossico 13353	. . . . . . . . . 10 ⊢ (((0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
37	28, 29, 31, 35, 36	syl22anc 838	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
38		imass2 6062	. . . . . . . . 9 ⊢ ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
39	17, 37, 38	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
40		sseq1 3969	. . . . . . . . 9 ⊢ (𝑤 = (^◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))))
41	40	rspcev 3585	. . . . . . . 8 ⊢ (((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
42	26, 39, 41	syl2anc 584	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
43		elfg 23791	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))))
44	43	biimpar 477	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
45	12, 16, 42, 44	syl12anc 836	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
46		cfiluexsm 24210	. . . . . 6 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ∧ (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
47	9, 10, 45, 46	syl3anc 1373	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
48		funimass2 6583	. . . . . . 7 ⊢ ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
49	48	ex 412	. . . . . 6 ⊢ (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
50	49	reximdv 3148	. . . . 5 ⊢ (Fun 𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
51	8, 47, 50	sylc 65	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
52	51	ralrimiva 3125	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
53	4, 52	jca 511	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
54		simprl 770	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
55		oveq2 7377	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
56	55	sseq2d 3976	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
57	56	rexbidv 3157	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
58		simp-4r 783	. . . . . . . . 9 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
59	58	simprd 495	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
60		simplr 768	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ⁺)
61	57, 59, 60	rspcdva 3586	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
62		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
63		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋)
64		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦ℝ⁺
65		nfre1 3260	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
66	64, 65	nfralw 3283	. . . . . . . . . . . . 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 23753	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
77	75, 76	sylancom 588	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
78		xpss12 5646	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
79	77, 77, 78	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
80		simp-6r 787	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋))
81	80, 6, 14	3syl 18	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋))
82	79, 81	sseqtrrd 3981	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
83	82	ex 412	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
84	74, 83	ralrimi 3233	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
85		r19.29r 3096	. . . . . . . 8 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
86		sseqin2 4182	. . . . . . . . . . . . 13 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
87	86	biimpi 216	. . . . . . . . . . . 12 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
88	87	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
89		dminss 6114	. . . . . . . . . . 11 ⊢ (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
90	88, 89	eqsstrrdi 3989	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
91		imass2 6062	. . . . . . . . . . 11 ⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
92	91	adantr 480	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
93	90, 92	sstrd 3954	. . . . . . . . 9 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
94	93	reximi 3067	. . . . . . . 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 3165	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
98		sstr 3952	. . . . . . . 8 ⊢ (((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
99	98	reximi 3067	. . . . . . 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 785	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝐷 ∈ (PsMet‘𝑋))
103		simplr 768	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹)
104	1	metustel 24471	. . . . . . . . 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 3165	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣))
108		sseq1 3969	. . . . . . . . . 10 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
109	108	biimpa 476	. . . . . . . . 9 ⊢ ((𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
110	109	reximi 3067	. . . . . . . 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 23791	. . . . . . . . 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 3141	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
119	101, 118	r19.29a 3141	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
120	119	ralrimiva 3125	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
121	2	adantr 480	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
122		iscfilu 24208	. . . 4 ⊢ (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
123	121, 122	syl 17	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
124	54, 120, 123	mpbir2and 713	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
125	53, 124	impbida 800	1 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 class class class wbr 5102 ↦ cmpt 5183 × cxp 5629 ^◡ccnv 5630 dom cdm 5631 ran crn 5632 “ cima 5634 Fun wfun 6493 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 0cc0 11044 ℝ^*cxr 11183 ≤ cle 11185 / cdiv 11811 2c2 12217 ℝ⁺crp 12927 [,)cico 13284 PsMetcpsmet 21280 fBascfbas 21284 filGencfg 21285 UnifOncust 24120 CauFil_uccfilu 24206

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ico 13288 df-psmet 21288 df-fbas 21293 df-fg 21294 df-fil 23766 df-ust 24121 df-cfilu 24207

This theorem is referenced by: cfilucfil2 24482

W3C validator