metustfbas

Description: The filter base generated by a metric D . (Contributed by Thierry Arnoux, 26-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Hypothesis	metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
	Assertion	metustfbas	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2	1	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
3		simpr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
4		cnvimass	⊢ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ dom 𝐷
5		psmetf	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
6	5	fdmd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
7	6	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
8	4 7	sseqtrid	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) )
9	3 8	eqsstrd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
10	9	ex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
11	10	rexlimdvw	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
12	2 11	sylbid	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
13	12	ralrimiv	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
14		pwssb	⊢ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ ∀ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
15	13 14	sylibr	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
16	15	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
17		cnvexg	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ^◡ 𝐷 ∈ V )
18		imaexg	⊢ ( ^◡ 𝐷 ∈ V → ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) ∈ V )
19		elisset	⊢ ( ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) ∈ V → ∃ 𝑥 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) )
20		1rp	⊢ 1 ∈ ℝ⁺
21		oveq2	⊢ ( 𝑎 = 1 → ( 0 [,) 𝑎 ) = ( 0 [,) 1 ) )
22	21	imaeq2d	⊢ ( 𝑎 = 1 → ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) )
23	22	rspceeqv	⊢ ( ( 1 ∈ ℝ⁺ ∧ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) ) → ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
24	20 23	mpan	⊢ ( 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) → ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
25	24	eximi	⊢ ( ∃ 𝑥 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 1 ) ) → ∃ 𝑥 ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
26	17 18 19 25	4syl	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
27	2	exbidv	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ 𝐹 ↔ ∃ 𝑥 ∃ 𝑎 ∈ ℝ⁺ 𝑥 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
28	26 27	mpbird	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 𝑥 ∈ 𝐹 )
29	28	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑥 𝑥 ∈ 𝐹 )
30		n0	⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐹 )
31	29 30	sylibr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ≠ ∅ )
32	1	metustid	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝑥 )
33	32	adantll	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝑥 )
34		n0	⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ 𝑋 )
35	34	biimpi	⊢ ( 𝑋 ≠ ∅ → ∃ 𝑝 𝑝 ∈ 𝑋 )
36	35	adantr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑝 𝑝 ∈ 𝑋 )
37		opelidres	⊢ ( 𝑝 ∈ 𝑋 → ( ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝑝 ∈ 𝑋 ) )
38	37	ibir	⊢ ( 𝑝 ∈ 𝑋 → ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) )
39	38	ne0d	⊢ ( 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
40	39	exlimiv	⊢ ( ∃ 𝑝 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
41	36 40	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( I ↾ 𝑋 ) ≠ ∅ )
42	41	adantr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ≠ ∅ )
43		ssn0	⊢ ( ( ( I ↾ 𝑋 ) ⊆ 𝑥 ∧ ( I ↾ 𝑋 ) ≠ ∅ ) → 𝑥 ≠ ∅ )
44	33 42 43	syl2anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ≠ ∅ )
45	44	nelrdva	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝐹 )
46		df-nel	⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 )
47	45 46	sylibr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∅ ∉ 𝐹 )
48		dfss2	⊢ ( 𝑥 ⊆ 𝑦 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑥 )
49	48	biimpi	⊢ ( 𝑥 ⊆ 𝑦 → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
50	49	adantl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
51		simplrl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ 𝐹 )
52	50 51	eqeltrd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
53		sseqin2	⊢ ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑦 )
54	53	biimpi	⊢ ( 𝑦 ⊆ 𝑥 → ( 𝑥 ∩ 𝑦 ) = 𝑦 )
55	54	adantl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) = 𝑦 )
56		simplrr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝐹 )
57	55 56	eqeltrd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
58		simplr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
59		simprl	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐹 )
60		simprr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐹 )
61	1	metustto	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
62	58 59 60 61	syl3anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
63	52 57 62	mpjaodan	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
64		ssidd	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
65		sseq1	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
66	65	rspcev	⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
67	63 64 66	syl2anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
68	67	ralrimivva	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
69	31 47 68	3jca	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
70		elfvex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
71	70	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝑋 ∈ V )
72	71 71	xpexd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ V )
73		isfbas2	⊢ ( ( 𝑋 × 𝑋 ) ∈ V → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
74	72 73	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
75	16 69 74	mpbir2and	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )

Metamath Proof Explorer

Theorem metustfbas

Proof