cfilucfil

Description: Given a metric D 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 . (Contributed by Thierry Arnoux, 29-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
	Assertion	cfilucfil	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2	1	metust	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
3		cfilufbas	⊢ ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
4	2 3	sylan	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
5		simpllr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
6		psmetf	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
7		ffun	⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* → Fun 𝐷 )
8	5 6 7	3syl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → Fun 𝐷 )
9	2	ad2antrr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
10		simplr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
11	1	metustfbas	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
12	11	ad2antrr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
13		cnvimass	⊢ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ dom 𝐷
14		fdm	⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
15	5 6 14	3syl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
16	13 15	sseqtrid	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) )
17		simpr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝑥 ∈ ℝ⁺ )
18	17	rphalfcld	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝑥 / 2 ) ∈ ℝ⁺ )
19		eqidd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) )
20		oveq2	⊢ ( 𝑎 = ( 𝑥 / 2 ) → ( 0 [,) 𝑎 ) = ( 0 [,) ( 𝑥 / 2 ) ) )
21	20	imaeq2d	⊢ ( 𝑎 = ( 𝑥 / 2 ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) )
22	21	rspceeqv	⊢ ( ( ( 𝑥 / 2 ) ∈ ℝ⁺ ∧ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
23	18 19 22	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
24	1	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
25	24	biimpar	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 )
26	5 23 25	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 )
27		0xr	⊢ 0 ∈ ℝ^*
28	27	a1i	⊢ ( 𝑥 ∈ ℝ⁺ → 0 ∈ ℝ^* )
29		rpxr	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^* )
30		0le0	⊢ 0 ≤ 0
31	30	a1i	⊢ ( 𝑥 ∈ ℝ⁺ → 0 ≤ 0 )
32		rpre	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ )
33	32	rehalfcld	⊢ ( 𝑥 ∈ ℝ⁺ → ( 𝑥 / 2 ) ∈ ℝ )
34		rphalflt	⊢ ( 𝑥 ∈ ℝ⁺ → ( 𝑥 / 2 ) < 𝑥 )
35	33 32 34	ltled	⊢ ( 𝑥 ∈ ℝ⁺ → ( 𝑥 / 2 ) ≤ 𝑥 )
36		icossico	⊢ ( ( ( 0 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) ∧ ( 0 ≤ 0 ∧ ( 𝑥 / 2 ) ≤ 𝑥 ) ) → ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) )
37	28 29 31 35 36	syl22anc	⊢ ( 𝑥 ∈ ℝ⁺ → ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) )
38		imass2	⊢ ( ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
39	17 37 38	3syl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
40		sseq1	⊢ ( 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) → ( 𝑤 ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ↔ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ) )
41	40	rspcev	⊢ ( ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 ∧ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ) → ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
42	26 39 41	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
43		elfg	⊢ ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ↔ ( ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ) ) )
44	43	biimpar	⊢ ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ ( ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
45	12 16 42 44	syl12anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
46		cfiluexsm	⊢ ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
47	9 10 45 46	syl3anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) )
48		funimass2	⊢ ( ( Fun 𝐷 ∧ ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) ) → ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
49	48	ex	⊢ ( Fun 𝐷 → ( ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) → ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
50	49	reximdv	⊢ ( Fun 𝐷 → ( ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑥 ) ) → ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
51	8 47 50	sylc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
52	51	ralrimiva	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
53	4 52	jca	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
54		simprl	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
55		oveq2	⊢ ( 𝑥 = 𝑎 → ( 0 [,) 𝑥 ) = ( 0 [,) 𝑎 ) )
56	55	sseq2d	⊢ ( 𝑥 = 𝑎 → ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ) )
57	56	rexbidv	⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ) )
58		simp-4r	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
59	58	simprd	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
60		simplr	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → 𝑎 ∈ ℝ⁺ )
61	57 59 60	rspcdva	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) )
62		nfv	⊢ Ⅎ 𝑦 ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
63		nfv	⊢ Ⅎ 𝑦 𝐶 ∈ ( fBas ‘ 𝑋 )
64		nfcv	⊢ Ⅎ 𝑦 ℝ⁺
65		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
66	64 65	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
67	63 66	nfan	⊢ Ⅎ 𝑦 ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
68	62 67	nfan	⊢ Ⅎ 𝑦 ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
69		nfv	⊢ Ⅎ 𝑦 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 )
70	68 69	nfan	⊢ Ⅎ 𝑦 ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
71		nfv	⊢ Ⅎ 𝑦 𝑎 ∈ ℝ⁺
72	70 71	nfan	⊢ Ⅎ 𝑦 ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ )
73		nfv	⊢ Ⅎ 𝑦 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣
74	72 73	nfan	⊢ Ⅎ 𝑦 ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
75	54	ad4antr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
76		fbelss	⊢ ( ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ⊆ 𝑋 )
77	75 76	sylancom	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ⊆ 𝑋 )
78		xpss12	⊢ ( ( 𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
79	77 77 78	syl2anc	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
80		simp-6r	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
81	80 6 14	3syl	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
82	79 81	sseqtrrd	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 )
83	82	ex	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝑦 ∈ 𝐶 → ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) )
84	74 83	ralrimi	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∀ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 )
85		r19.29r	⊢ ( ( ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦 ∈ 𝐶 ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) )
86		sseqin2	⊢ ( ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ↔ ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
87	86	biimpi	⊢ ( ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 → ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
88	87	adantl	⊢ ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
89		dminss	⊢ ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) ⊆ ( ^◡ 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) )
90	88 89	eqsstrrdi	⊢ ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) )
91		imass2	⊢ ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) → ( ^◡ 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
92	91	adantr	⊢ ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( ^◡ 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
93	90 92	sstrd	⊢ ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
94	93	reximi	⊢ ( ∃ 𝑦 ∈ 𝐶 ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
95	85 94	syl	⊢ ( ( ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
96	61 84 95	syl2anc	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
97		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐶 ( ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ↔ ( ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) )
98		sstr	⊢ ( ( ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
99	98	reximi	⊢ ( ∃ 𝑦 ∈ 𝐶 ( ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
100	97 99	sylbir	⊢ ( ( ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
101	96 100	sylancom	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
102		simp-5r	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝐹 ) ∧ 𝑤 ⊆ 𝑣 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
103		simplr	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝐹 ) ∧ 𝑤 ⊆ 𝑣 ) → 𝑤 ∈ 𝐹 )
104	1	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑤 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ⁺ 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
105	104	biimpa	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐹 ) → ∃ 𝑎 ∈ ℝ⁺ 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
106	102 103 105	syl2anc	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝐹 ) ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ⁺ 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
107		r19.41v	⊢ ( ∃ 𝑎 ∈ ℝ⁺ ( 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤 ⊆ 𝑣 ) ↔ ( ∃ 𝑎 ∈ ℝ⁺ 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤 ⊆ 𝑣 ) )
108		sseq1	⊢ ( 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → ( 𝑤 ⊆ 𝑣 ↔ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) )
109	108	biimpa	⊢ ( ( 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤 ⊆ 𝑣 ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
110	109	reximi	⊢ ( ∃ 𝑎 ∈ ℝ⁺ ( 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
111	107 110	sylbir	⊢ ( ( ∃ 𝑎 ∈ ℝ⁺ 𝑤 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
112	106 111	sylancom	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝐹 ) ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
113	11	ad2antrr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
114		elfg	⊢ ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ↔ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) ) )
115	114	biimpa	⊢ ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) )
116	113 115	sylancom	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) )
117	116	simprd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 )
118	112 117	r19.29a	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑎 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
119	101 118	r19.29a	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
120	119	ralrimiva	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
121	2	adantr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
122		iscfilu	⊢ ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 ) ) )
123	121 122	syl	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦 ∈ 𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 ) ) )
124	54 120 123	mpbir2and	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
125	53 124	impbida	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem cfilucfil

Proof