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 24474

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 25192. (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 24473	. . . 4 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3		cfilufbas 24203	. . . 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 24221	. . . . . 6 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
7		ffun 6654	. . . . . 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 24472	. . . . . . . 8 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
12	11	ad2antrr 726	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13		cnvimass 6030	. . . . . . . 8 ⊢ (^◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14		fdm 6660	. . . . . . . . 9 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → dom 𝐷 = (𝑋 × 𝑋))
15	5, 6, 14	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → dom 𝐷 = (𝑋 × 𝑋))
16	13, 15	sseqtrid 3972	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
18	17	rphalfcld 12946	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
19		eqidd 2732	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
20		oveq2 7354	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
21	20	imaeq2d 6008	. . . . . . . . . . 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 24465	. . . . . . . . . 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 11159	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^*)
29		rpxr 12900	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
30		0le0 12226	. . . . . . . . . . 11 ⊢ 0 ≤ 0
31	30	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ 0)
32		rpre 12899	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
33	32	rehalfcld 12368	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
34		rphalflt 12921	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
35	33, 32, 34	ltled 11261	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ≤ 𝑥)
36		icossico 13316	. . . . . . . . . 10 ⊢ (((0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
37	28, 29, 31, 35, 36	syl22anc 838	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
38		imass2 6050	. . . . . . . . 9 ⊢ ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
39	17, 37, 38	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
40		sseq1 3955	. . . . . . . . 9 ⊢ (𝑤 = (^◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))))
41	40	rspcev 3572	. . . . . . . 8 ⊢ (((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
42	26, 39, 41	syl2anc 584	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
43		elfg 23786	. . . . . . . 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 24204	. . . . . 6 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ∧ (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
47	9, 10, 45, 46	syl3anc 1373	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
48		funimass2 6564	. . . . . . 7 ⊢ ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
49	48	ex 412	. . . . . 6 ⊢ (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
50	49	reximdv 3147	. . . . 5 ⊢ (Fun 𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
51	8, 47, 50	sylc 65	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
52	51	ralrimiva 3124	. . 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 7354	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
56	55	sseq2d 3962	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
57	56	rexbidv 3156	. . . . . . . 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 3573	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
62		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
63		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋)
64		nfcv 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦ℝ⁺
65		nfre1 3257	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
66	64, 65	nfralw 3279	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
67	63, 66	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
68	62, 67	nfan 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
69		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
70	68, 69	nfan 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
71		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑎 ∈ ℝ⁺
72	70, 71	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺)
73		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑦(^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣
74	72, 73	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
75	54	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋))
76		fbelss 23748	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
77	75, 76	sylancom 588	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
78		xpss12 5629	. . . . . . . . . . 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 3967	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
83	82	ex 412	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
84	74, 83	ralrimi 3230	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
85		r19.29r 3096	. . . . . . . 8 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
86		sseqin2 4170	. . . . . . . . . . . . 13 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
87	86	biimpi 216	. . . . . . . . . . . 12 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
88	87	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
89		dminss 6100	. . . . . . . . . . 11 ⊢ (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
90	88, 89	eqsstrrdi 3975	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
91		imass2 6050	. . . . . . . . . . 11 ⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
92	91	adantr 480	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
93	90, 92	sstrd 3940	. . . . . . . . 9 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
94	93	reximi 3070	. . . . . . . 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 3162	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
98		sstr 3938	. . . . . . . 8 ⊢ (((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
99	98	reximi 3070	. . . . . . 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 24465	. . . . . . . . 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 3162	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣))
108		sseq1 3955	. . . . . . . . . 10 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
109	108	biimpa 476	. . . . . . . . 9 ⊢ ((𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
110	109	reximi 3070	. . . . . . . 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 23786	. . . . . . . . 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 3140	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
119	101, 118	r19.29a 3140	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
120	119	ralrimiva 3124	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
121	2	adantr 480	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
122		iscfilu 24202	. . . 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 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 class class class wbr 5089 ↦ cmpt 5170 × cxp 5612 ^◡ccnv 5613 dom cdm 5614 ran crn 5615 “ cima 5617 Fun wfun 6475 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 0cc0 11006 ℝ^*cxr 11145 ≤ cle 11147 / cdiv 11774 2c2 12180 ℝ⁺crp 12890 [,)cico 13247 PsMetcpsmet 21275 fBascfbas 21279 filGencfg 21280 UnifOncust 24115 CauFil_uccfilu 24200

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ico 13251 df-psmet 21283 df-fbas 21288 df-fg 21289 df-fil 23761 df-ust 24116 df-cfilu 24201

This theorem is referenced by: cfilucfil2 24476

W3C validator