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 23915

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 24629. (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 23914	. . . 4 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3		cfilufbas 23641	. . . 4 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
4	2, 3	sylan 580	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5		simpllr 774	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ (PsMet‘𝑋))
6		psmetf 23659	. . . . . 6 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
7		ffun 6671	. . . . . 6 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → Fun 𝐷)
8	5, 6, 7	3syl 18	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → Fun 𝐷)
9	2	ad2antrr 724	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10		simplr 767	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
11	1	metustfbas 23913	. . . . . . . 8 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
12	11	ad2antrr 724	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13		cnvimass 6033	. . . . . . . 8 ⊢ (^◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14		fdm 6677	. . . . . . . . 9 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → dom 𝐷 = (𝑋 × 𝑋))
15	5, 6, 14	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → dom 𝐷 = (𝑋 × 𝑋))
16	13, 15	sseqtrid 3996	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
18	17	rphalfcld 12969	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
19		eqidd 2737	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
20		oveq2 7365	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
21	20	imaeq2d 6013	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 / 2) → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
22	21	rspceeqv 3595	. . . . . . . . . 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 23906	. . . . . . . . . 10 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))))
25	24	biimpar 478	. . . . . . . . 9 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
26	5, 23, 25	syl2anc 584	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
27		0xr 11202	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^*)
29		rpxr 12924	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
30		0le0 12254	. . . . . . . . . . 11 ⊢ 0 ≤ 0
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ 0)
32		rpre 12923	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
33	32	rehalfcld 12400	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
34		rphalflt 12944	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
35	33, 32, 34	ltled 11303	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ≤ 𝑥)
36		icossico 13334	. . . . . . . . . 10 ⊢ (((0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
37	28, 29, 31, 35, 36	syl22anc 837	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
38		imass2 6054	. . . . . . . . 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 3581	. . . . . . . 8 ⊢ (((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
42	26, 39, 41	syl2anc 584	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
43		elfg 23222	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))))
44	43	biimpar 478	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
45	12, 16, 42, 44	syl12anc 835	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
46		cfiluexsm 23642	. . . . . 6 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ∧ (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
47	9, 10, 45, 46	syl3anc 1371	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
48		funimass2 6584	. . . . . . 7 ⊢ ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
49	48	ex 413	. . . . . 6 ⊢ (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
50	49	reximdv 3167	. . . . 5 ⊢ (Fun 𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
51	8, 47, 50	sylc 65	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
52	51	ralrimiva 3143	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
53	4, 52	jca 512	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
54		simprl 769	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
55		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
56	55	sseq2d 3976	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
57	56	rexbidv 3175	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
58		simp-4r 782	. . . . . . . . 9 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
59	58	simprd 496	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
60		simplr 767	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ⁺)
61	57, 59, 60	rspcdva 3582	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
62		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
63		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋)
64		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦ℝ⁺
65		nfre1 3268	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
66	64, 65	nfralw 3294	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
67	63, 66	nfan 1902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
68	62, 67	nfan 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
69		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
70	68, 69	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
71		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑎 ∈ ℝ⁺
72	70, 71	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺)
73		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑦(^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣
74	72, 73	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
75	54	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋))
76		fbelss 23184	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
77	75, 76	sylancom 588	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
78		xpss12 5648	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
79	77, 77, 78	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
80		simp-6r 786	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋))
81	80, 6, 14	3syl 18	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋))
82	79, 81	sseqtrrd 3985	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
83	82	ex 413	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
84	74, 83	ralrimi 3240	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
85		r19.29r 3119	. . . . . . . 8 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
86		sseqin2 4175	. . . . . . . . . . . . 13 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
87	86	biimpi 215	. . . . . . . . . . . 12 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
88	87	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
89		dminss 6105	. . . . . . . . . . 11 ⊢ (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
90	88, 89	eqsstrrdi 3999	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
91		imass2 6054	. . . . . . . . . . 11 ⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
92	91	adantr 481	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
93	90, 92	sstrd 3954	. . . . . . . . 9 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
94	93	reximi 3087	. . . . . . . 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 3185	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
98		sstr 3952	. . . . . . . 8 ⊢ (((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
99	98	reximi 3087	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
100	97, 99	sylbir 234	. . . . . 6 ⊢ ((∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
101	96, 100	sylancom 588	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
102		simp-5r 784	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝐷 ∈ (PsMet‘𝑋))
103		simplr 767	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹)
104	1	metustel 23906	. . . . . . . . 9 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎))))
105	104	biimpa 477	. . . . . . . 8 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
106	102, 103, 105	syl2anc 584	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
107		r19.41v 3185	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣))
108		sseq1 3969	. . . . . . . . . 10 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
109	108	biimpa 477	. . . . . . . . 9 ⊢ ((𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
110	109	reximi 3087	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
111	107, 110	sylbir 234	. . . . . . 7 ⊢ ((∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
112	106, 111	sylancom 588	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
113	11	ad2antrr 724	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
114		elfg 23222	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)))
115	114	biimpa 477	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
116	113, 115	sylancom 588	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
117	116	simprd 496	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
118	112, 117	r19.29a 3159	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
119	101, 118	r19.29a 3159	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
120	119	ralrimiva 3143	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
121	2	adantr 481	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
122		iscfilu 23640	. . . 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 711	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
125	53, 124	impbida 799	1 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 “ cima 5636 Fun wfun 6490 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 0cc0 11051 ℝ^*cxr 11188 ≤ cle 11190 / cdiv 11812 2c2 12208 ℝ⁺crp 12915 [,)cico 13266 PsMetcpsmet 20780 fBascfbas 20784 filGencfg 20785 UnifOncust 23551 CauFil_uccfilu 23638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-po 5545 df-so 5546 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-1st 7921 df-2nd 7922 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-2 12216 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ico 13270 df-psmet 20788 df-fbas 20793 df-fg 20794 df-fil 23197 df-ust 23552 df-cfilu 23639

This theorem is referenced by: cfilucfil2 23917

W3C validator