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	birani	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑝 𝑝 ∈ 𝑋 )
36		opelidres	⊢ ( 𝑝 ∈ 𝑋 → ( ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝑝 ∈ 𝑋 ) )
37	36	ibir	⊢ ( 𝑝 ∈ 𝑋 → ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) )
38	37	ne0d	⊢ ( 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
39	38	exlimiv	⊢ ( ∃ 𝑝 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
40	35 39	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( I ↾ 𝑋 ) ≠ ∅ )
41	40	adantr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ≠ ∅ )
42		ssn0	⊢ ( ( ( I ↾ 𝑋 ) ⊆ 𝑥 ∧ ( I ↾ 𝑋 ) ≠ ∅ ) → 𝑥 ≠ ∅ )
43	33 41 42	syl2anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ≠ ∅ )
44	43	nelrdva	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝐹 )
45		df-nel	⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 )
46	44 45	sylibr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∅ ∉ 𝐹 )
47		dfss2	⊢ ( 𝑥 ⊆ 𝑦 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑥 )
48	47	bilani	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
49		simplrl	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ 𝐹 )
50	48 49	eqeltrd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
51		sseqin2	⊢ ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑦 )
52	51	bilani	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) = 𝑦 )
53		simplrr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝐹 )
54	52 53	eqeltrd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
55		simplr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
56		simprl	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐹 )
57		simprr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐹 )
58	1	metustto	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
59	55 56 57 58	syl3anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
60	50 54 59	mpjaodan	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
61		ssidd	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
62		sseq1	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
63	62	rspcev	⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
64	60 61 63	syl2anc	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
65	64	ralrimivva	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
66	31 46 65	3jca	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
67		elfvex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
68	67	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝑋 ∈ V )
69	68 68	xpexd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ V )
70		isfbas2	⊢ ( ( 𝑋 × 𝑋 ) ∈ V → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
71	69 70	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
72	16 66 71	mpbir2and	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )

Metamath Proof Explorer

Theorem metustfbas

Proof