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	birani	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \exists p p \in X$
36		opelidres	$⊢ p \in X \to (⟨p, p⟩ \in ({I ↾}_{X}) \leftrightarrow p \in X)$
37	36	ibir	$⊢ p \in X \to ⟨p, p⟩ \in ({I ↾}_{X})$
38	37	ne0d	$⊢ p \in X \to {I ↾}_{X} \neq \emptyset$
39	38	exlimiv	$⊢ \exists p p \in X \to {I ↾}_{X} \neq \emptyset$
40	35 39	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to {I ↾}_{X} \neq \emptyset$
41	40	adantr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land x \in F) \to {I ↾}_{X} \neq \emptyset$
42		ssn0	$⊢ ({I ↾}_{X} \subseteq x \land {I ↾}_{X} \neq \emptyset) \to x \neq \emptyset$
43	33 41 42	syl2anc	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land x \in F) \to x \neq \emptyset$
44	43	nelrdva	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \neg \emptyset \in F$
45		df-nel	$⊢ \emptyset \notin F \leftrightarrow \neg \emptyset \in F$
46	44 45	sylibr	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to \emptyset \notin F$
47		dfss2	$⊢ x \subseteq y \leftrightarrow x \cap y = x$
48	47	bilani	$⊢ (((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$
49		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$
50	48 49	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$
51		sseqin2	$⊢ y \subseteq x \leftrightarrow x \cap y = y$
52	51	bilani	$⊢ (((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$
53		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$
54	52 53	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$
55		simplr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to D \in PsMet (X)$
56		simprl	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to x \in F$
57		simprr	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to y \in F$
58	1	metustto	$⊢ (D \in PsMet (X) \land x \in F \land y \in F) \to (x \subseteq y \lor y \subseteq x)$
59	55 56 57 58	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)$
60	50 54 59	mpjaodan	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land (x \in F \land y \in F)) \to x \cap y \in F$
61		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$
62		sseq1	$⊢ z = x \cap y \to (z \subseteq x \cap y \leftrightarrow x \cap y \subseteq x \cap y)$
63	62	rspcev	$⊢ (x \cap y \in F \land x \cap y \subseteq x \cap y) \to \exists z \in F z \subseteq x \cap y$
64	60 61 63	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$
65	64	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$
66	31 46 65	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)$
67		elfvex	$⊢ D \in PsMet (X) \to X \in V$
68	67	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \in V$
69	68 68	xpexd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to X \times X \in V$
70		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)))$
71	69 70	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)))$
72	16 66 71	mpbir2and	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to F \in fBas (X \times X)$

Metamath Proof Explorer

Theorem metustfbas

Proof