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 22174

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 22871. (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 22173	. . . 4 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
3		cfilufbas 21903	. . . 4 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
4	2, 3	sylan 487	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → 𝐶 ∈ (fBas‘𝑋))
5		simpllr 795	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐷 ∈ (PsMet‘𝑋))
6		psmetf 21921	. . . . . 6 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
7		ffun 5961	. . . . . 6 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → Fun 𝐷)
8	5, 6, 7	3syl 18	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → Fun 𝐷)
9	2	ad2antrr 758	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
10		simplr 788	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
11	1	metustfbas 22172	. . . . . . . 8 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
12	11	ad2antrr 758	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
13		cnvimass 5404	. . . . . . . 8 ⊢ (^◡𝐷 “ (0[,)𝑥)) ⊆ dom 𝐷
14		fdm 5964	. . . . . . . . 9 ⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ^* → dom 𝐷 = (𝑋 × 𝑋))
15	5, 6, 14	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → dom 𝐷 = (𝑋 × 𝑋))
16	13, 15	syl5sseq 3616	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋))
17		simpr 476	. . . . . . . . . . 11 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
18	17	rphalfcld 11760	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
19		eqidd 2611	. . . . . . . . . 10 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
20		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑥 / 2) → (0[,)𝑎) = (0[,)(𝑥 / 2)))
21	20	imaeq2d 5385	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑥 / 2) → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)(𝑥 / 2))))
22	21	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑥 / 2) → ((^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2)))))
23	22	rspcev 3282	. . . . . . . . . 10 ⊢ (((𝑥 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)(𝑥 / 2)))) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
24	18, 19, 23	syl2anc 691	. . . . . . . . 9 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎)))
25	1	metustel 22165	. . . . . . . . . 10 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))))
26	25	biimpar 501	. . . . . . . . 9 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑥 / 2))) = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
27	5, 24, 26	syl2anc 691	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹)
28		0xr 9965	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
29	28	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^*)
30		rpxr 11716	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
31		0le0 10987	. . . . . . . . . . 11 ⊢ 0 ≤ 0
32	31	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ 0)
33		rpre 11715	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
34	33	rehalfcld 11156	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ)
35		rphalflt 11736	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
36	34, 33, 35	ltled 10064	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ≤ 𝑥)
37		icossico 12114	. . . . . . . . . 10 ⊢ (((0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) ∧ (0 ≤ 0 ∧ (𝑥 / 2) ≤ 𝑥)) → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
38	29, 30, 32, 36, 37	syl22anc 1319	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (0[,)(𝑥 / 2)) ⊆ (0[,)𝑥))
39		imass2 5420	. . . . . . . . 9 ⊢ ((0[,)(𝑥 / 2)) ⊆ (0[,)𝑥) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
40	17, 38, 39	3syl 18	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥)))
41		sseq1 3589	. . . . . . . . 9 ⊢ (𝑤 = (^◡𝐷 “ (0[,)(𝑥 / 2))) → (𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)) ↔ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))))
42	41	rspcev 3282	. . . . . . . 8 ⊢ (((^◡𝐷 “ (0[,)(𝑥 / 2))) ∈ 𝐹 ∧ (^◡𝐷 “ (0[,)(𝑥 / 2))) ⊆ (^◡𝐷 “ (0[,)𝑥))) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
43	27, 40, 42	syl2anc 691	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))
44		elfg 21485	. . . . . . . 8 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → ((^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))))
45	44	biimpar 501	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ((^◡𝐷 “ (0[,)𝑥)) ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ (^◡𝐷 “ (0[,)𝑥)))) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
46	12, 16, 43, 45	syl12anc 1316	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹))
47		cfiluexsm 21904	. . . . . 6 ⊢ ((((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ∧ (^◡𝐷 “ (0[,)𝑥)) ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
48	9, 10, 46, 47	syl3anc 1318	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)))
49		funimass2 5886	. . . . . . 7 ⊢ ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥))) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
50	49	ex 449	. . . . . 6 ⊢ (Fun 𝐷 → ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
51	50	reximdv 2999	. . . . 5 ⊢ (Fun 𝐷 → (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑥)) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
52	8, 48, 51	sylc 63	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
53	52	ralrimiva 2949	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
54	4, 53	jca 553	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹))) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
55		simprl 790	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (fBas‘𝑋))
56		simp-4r 803	. . . . . . . . 9 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
57	56	simprd 478	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
58		simplr 788	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → 𝑎 ∈ ℝ⁺)
59		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (0[,)𝑥) = (0[,)𝑎))
60	59	sseq2d 3596	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
61	60	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
62	61	rspccv 3279	. . . . . . . 8 ⊢ (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) → (𝑎 ∈ ℝ⁺ → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎)))
63	57, 58, 62	sylc 63	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎))
64		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))
65		nfv 1830	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝐶 ∈ (fBas‘𝑋)
66		nfcv 2751	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦ℝ⁺
67		nfre1 2988	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
68	66, 67	nfral 2929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
69	65, 68	nfan 1816	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))
70	64, 69	nfan 1816	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))
71		nfv 1830	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)
72	70, 71	nfan 1816	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹))
73		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑎 ∈ ℝ⁺
74	72, 73	nfan 1816	. . . . . . . . 9 ⊢ Ⅎ𝑦((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺)
75		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑦(^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣
76	74, 75	nfan 1816	. . . . . . . 8 ⊢ Ⅎ𝑦(((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
77	55	ad4antr 764	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐶 ∈ (fBas‘𝑋))
78		fbelss 21447	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
79	77, 78	sylancom 698	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝑦 ⊆ 𝑋)
80		xpss12 5148	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
81	79, 79, 80	syl2anc 691	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
82		simp-6r 807	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → 𝐷 ∈ (PsMet‘𝑋))
83	82, 6, 14	3syl 18	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → dom 𝐷 = (𝑋 × 𝑋))
84	81, 83	sseqtr4d 3605	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ∧ 𝑦 ∈ 𝐶) → (𝑦 × 𝑦) ⊆ dom 𝐷)
85	84	ex 449	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 ∈ 𝐶 → (𝑦 × 𝑦) ⊆ dom 𝐷))
86	76, 85	ralrimi 2940	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷)
87		r19.29r 3055	. . . . . . . 8 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷))
88		sseqin2 3779	. . . . . . . . . . . . 13 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 ↔ (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
89	88	biimpi 205	. . . . . . . . . . . 12 ⊢ ((𝑦 × 𝑦) ⊆ dom 𝐷 → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
90	89	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (dom 𝐷 ∩ (𝑦 × 𝑦)) = (𝑦 × 𝑦))
91		dminss 5466	. . . . . . . . . . 11 ⊢ (dom 𝐷 ∩ (𝑦 × 𝑦)) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦)))
92	90, 91	syl6eqssr 3619	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))))
93		imass2 5420	. . . . . . . . . . 11 ⊢ ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
94	93	adantr 480	. . . . . . . . . 10 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (^◡𝐷 “ (𝐷 “ (𝑦 × 𝑦))) ⊆ (^◡𝐷 “ (0[,)𝑎)))
95	92, 94	sstrd 3578	. . . . . . . . 9 ⊢ (((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
96	95	reximi 2994	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐶 ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
97	87, 96	syl 17	. . . . . . 7 ⊢ ((∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑎) ∧ ∀𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ dom 𝐷) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
98	63, 86, 97	syl2anc 691	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)))
99		r19.41v 3070	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) ↔ (∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
100		sstr 3576	. . . . . . . 8 ⊢ (((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → (𝑦 × 𝑦) ⊆ 𝑣)
101	100	reximi 2994	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝐶 ((𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
102	99, 101	sylbir 224	. . . . . 6 ⊢ ((∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ (^◡𝐷 “ (0[,)𝑎)) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
103	98, 102	sylancom 698	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑎 ∈ ℝ⁺) ∧ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
104		simp-5r 805	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝐷 ∈ (PsMet‘𝑋))
105		simplr 788	. . . . . . . 8 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → 𝑤 ∈ 𝐹)
106	1	metustel 22165	. . . . . . . . 9 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑤 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎))))
107	106	biimpa 500	. . . . . . . 8 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑤 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
108	104, 105, 107	syl2anc 691	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)))
109		r19.41v 3070	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) ↔ (∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣))
110		sseq1 3589	. . . . . . . . . 10 ⊢ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) → (𝑤 ⊆ 𝑣 ↔ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣))
111	110	biimpa 500	. . . . . . . . 9 ⊢ ((𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
112	111	reximi 2994	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ⁺ (𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
113	109, 112	sylbir 224	. . . . . . 7 ⊢ ((∃𝑎 ∈ ℝ⁺ 𝑤 = (^◡𝐷 “ (0[,)𝑎)) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
114	108, 113	sylancom 698	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) ∧ 𝑤 ∈ 𝐹) ∧ 𝑤 ⊆ 𝑣) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
115	11	ad2antrr 758	. . . . . . . 8 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
116		elfg 21485	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘(𝑋 × 𝑋)) → (𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹) ↔ (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)))
117	116	biimpa 500	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘(𝑋 × 𝑋)) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
118	115, 117	sylancom 698	. . . . . . 7 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → (𝑣 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
119	118	simprd 478	. . . . . 6 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
120	114, 119	r19.29a 3060	. . . . 5 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑎 ∈ ℝ⁺ (^◡𝐷 “ (0[,)𝑎)) ⊆ 𝑣)
121	103, 120	r19.29a 3060	. . . 4 ⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) ∧ 𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)) → ∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
122	121	ralrimiva 2949	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)
123	2	adantr 480	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
124		iscfilu 21902	. . . 4 ⊢ (((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
125	123, 124	syl 17	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ ((𝑋 × 𝑋)filGen𝐹)∃𝑦 ∈ 𝐶 (𝑦 × 𝑦) ⊆ 𝑣)))
126	55, 122, 125	mpbir2and 959	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)))
127	54, 126	impbida 873	1 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFil_u‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 “ cima 5041 Fun wfun 5798 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 0cc0 9815 ℝ^*cxr 9952 ≤ cle 9954 / cdiv 10563 2c2 10947 ℝ⁺crp 11708 [,)cico 12048 PsMetcpsmet 19551 fBascfbas 19555 filGencfg 19556 UnifOncust 21813 CauFil_uccfilu 21900

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-po 4959 df-so 4960 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-2 10956 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ico 12052 df-psmet 19559 df-fbas 19564 df-fg 19565 df-fil 21460 df-ust 21814 df-cfilu 21901

This theorem is referenced by: cfilucfil2 22176

W3C validator