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	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustfbas	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \in fBas (X \times X)$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	metustel	$⊢ D \in PsMet (X) \to (x \in F \leftrightarrow \exists a \in ℝ^{+} x = D^{-1} [[0, a)])$
3		simpr	$⊢ (D \in PsMet (X) \land x = D^{-1} [[0, a)]) \to x = D^{-1} [[0, a)]$
4		cnvimass	$⊢ D^{-1} [[0, a)] \subseteq dom D$
5		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
6	5	fdmd	$⊢ D \in PsMet (X) \to dom D = X \times X$
7	6	adantr	$⊢ (D \in PsMet (X) \land x = D^{-1} [[0, a)]) \to dom D = X \times X$
8	4 7	sseqtrid	$⊢ (D \in PsMet (X) \land x = D^{-1} [[0, a)]) \to D^{-1} [[0, a)] \subseteq X \times X$
9	3 8	eqsstrd	$⊢ (D \in PsMet (X) \land x = D^{-1} [[0, a)]) \to x \subseteq X \times X$
10	9	ex	$⊢ D \in PsMet (X) \to (x = D^{-1} [[0, a)] \to x \subseteq X \times X)$
11	10	rexlimdvw	$⊢ D \in PsMet (X) \to (\exists a \in ℝ^{+} x = D^{-1} [[0, a)] \to x \subseteq X \times X)$
12	2 11	sylbid	$⊢ D \in PsMet (X) \to (x \in F \to x \subseteq X \times X)$
13	12	ralrimiv	$⊢ D \in PsMet (X) \to \forall x \in F x \subseteq X \times X$
14		pwssb	$⊢ F \subseteq 𝒫 (X \times X) \leftrightarrow \forall x \in F x \subseteq X \times X$
15	13 14	sylibr	$⊢ D \in PsMet (X) \to F \subseteq 𝒫 (X \times X)$
16	15	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \subseteq 𝒫 (X \times X)$
17		cnvexg	$⊢ D \in PsMet (X) \to D^{-1} \in V$
18		imaexg	$⊢ D^{-1} \in V \to D^{-1} [[0, 1)] \in V$
19		elisset	$⊢ D^{-1} [[0, 1)] \in V \to \exists x x = D^{-1} [[0, 1)]$
20		1rp	$⊢ 1 \in ℝ^{+}$
21		oveq2	$⊢ a = 1 \to [0, a) = [0, 1)$
22	21	imaeq2d	$⊢ a = 1 \to D^{-1} [[0, a)] = D^{-1} [[0, 1)]$
23	22	rspceeqv	$⊢ (1 \in ℝ^{+} \land x = D^{-1} [[0, 1)]) \to \exists a \in ℝ^{+} x = D^{-1} [[0, a)]$
24	20 23	mpan	$⊢ x = D^{-1} [[0, 1)] \to \exists a \in ℝ^{+} x = D^{-1} [[0, a)]$
25	24	eximi	$⊢ \exists x x = D^{-1} [[0, 1)] \to \exists x \exists a \in ℝ^{+} x = D^{-1} [[0, a)]$
26	17 18 19 25	4syl	$⊢ D \in PsMet (X) \to \exists x \exists a \in ℝ^{+} x = D^{-1} [[0, a)]$
27	2	exbidv	$⊢ D \in PsMet (X) \to (\exists x x \in F \leftrightarrow \exists x \exists a \in ℝ^{+} x = D^{-1} [[0, a)])$
28	26 27	mpbird	$⊢ D \in PsMet (X) \to \exists x x \in F$
29	28	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \exists x x \in F$
30		n0	$⊢ F \neq \emptyset \leftrightarrow \exists x x \in F$
31	29 30	sylibr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \neq \emptyset$
32	1	metustid	$⊢ (D \in PsMet (X) \land x \in F) \to {I ↾}_{X} \subseteq x$
33	32	adantll	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land x \in F) \to {I ↾}_{X} \subseteq x$
34		n0	$⊢ X \neq \emptyset \leftrightarrow \exists p p \in X$
35	34	biimpi	$⊢ X \neq \emptyset \to \exists p p \in X$
36	35	adantr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \exists p p \in X$
37		opelidres	$⊢ p \in X \to (⟨p, p⟩ \in ({I ↾}_{X}) \leftrightarrow p \in X)$
38	37	ibir	$⊢ p \in X \to ⟨p, p⟩ \in ({I ↾}_{X})$
39	38	ne0d	$⊢ p \in X \to {I ↾}_{X} \neq \emptyset$
40	39	exlimiv	$⊢ \exists p p \in X \to {I ↾}_{X} \neq \emptyset$
41	36 40	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to {I ↾}_{X} \neq \emptyset$
42	41	adantr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land x \in F) \to {I ↾}_{X} \neq \emptyset$
43		ssn0	$⊢ ({I ↾}_{X} \subseteq x \land {I ↾}_{X} \neq \emptyset) \to x \neq \emptyset$
44	33 42 43	syl2anc	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land x \in F) \to x \neq \emptyset$
45	44	nelrdva	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \neg \emptyset \in F$
46		df-nel	$⊢ \emptyset \notin F \leftrightarrow \neg \emptyset \in F$
47	45 46	sylibr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \emptyset \notin F$
48		dfss2	$⊢ x \subseteq y \leftrightarrow x \cap y = x$
49	48	biimpi	$⊢ x \subseteq y \to x \cap y = x$
50	49	adantl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land x \subseteq y) \to x \cap y = x$
51		simplrl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land x \subseteq y) \to x \in F$
52	50 51	eqeltrd	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land x \subseteq y) \to x \cap y \in F$
53		sseqin2	$⊢ y \subseteq x \leftrightarrow x \cap y = y$
54	53	biimpi	$⊢ y \subseteq x \to x \cap y = y$
55	54	adantl	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land y \subseteq x) \to x \cap y = y$
56		simplrr	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land y \subseteq x) \to y \in F$
57	55 56	eqeltrd	$⊢ (((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \land y \subseteq x) \to x \cap y \in F$
58		simplr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to D \in PsMet (X)$
59		simprl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to x \in F$
60		simprr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to y \in F$
61	1	metustto	$⊢ (D \in PsMet (X) \land x \in F \land y \in F) \to (x \subseteq y \lor y \subseteq x)$
62	58 59 60 61	syl3anc	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to (x \subseteq y \lor y \subseteq x)$
63	52 57 62	mpjaodan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to x \cap y \in F$
64		ssidd	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to x \cap y \subseteq x \cap y$
65		sseq1	$⊢ z = x \cap y \to (z \subseteq x \cap y \leftrightarrow x \cap y \subseteq x \cap y)$
66	65	rspcev	$⊢ (x \cap y \in F \land x \cap y \subseteq x \cap y) \to \exists z \in F z \subseteq x \cap y$
67	63 64 66	syl2anc	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to \exists z \in F z \subseteq x \cap y$
68	67	ralrimivva	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y$
69	31 47 68	3jca	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)$
70		elfvex	$⊢ D \in PsMet (X) \to X \in V$
71	70	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \in V$
72	71 71	xpexd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \times X \in V$
73		isfbas2	$⊢ X \times X \in V \to (F \in fBas (X \times X) \leftrightarrow (F \subseteq 𝒫 (X \times X) \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)))$
74	72 73	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (F \in fBas (X \times X) \leftrightarrow (F \subseteq 𝒫 (X \times X) \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)))$
75	16 69 74	mpbir2and	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \in fBas (X \times X)$

Metamath Proof Explorer

Theorem metustfbas

Proof