metustid

Description: The identity diagonal is included in all elements of the filter base generated by the metric D . (Contributed by Thierry Arnoux, 22-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	metustid	$⊢ (D \in PsMet (X) \land A \in F) \to {I ↾}_{X} \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2		relres	$⊢ Rel ({I ↾}_{X})$
3	2	a1i	$⊢ (D \in PsMet (X) \land A \in F) \to Rel ({I ↾}_{X})$
4		vex	$⊢ q \in V$
5	4	brresi	$⊢ p ({I ↾}_{X}) q \leftrightarrow (p \in X \land p I q)$
6		df-br	$⊢ p ({I ↾}_{X}) q \leftrightarrow ⟨p, q⟩ \in ({I ↾}_{X})$
7	4	ideq	$⊢ p I q \leftrightarrow p = q$
8	7	anbi2i	$⊢ (p \in X \land p I q) \leftrightarrow (p \in X \land p = q)$
9	5 6 8	3bitr3i	$⊢ ⟨p, q⟩ \in ({I ↾}_{X}) \leftrightarrow (p \in X \land p = q)$
10	9	biimpi	$⊢ ⟨p, q⟩ \in ({I ↾}_{X}) \to (p \in X \land p = q)$
11	10	ad2antlr	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to (p \in X \land p = q)$
12	11	simprd	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to p = q$
13		df-ov	$⊢ p D p = D (⟨p, p⟩)$
14		opeq2	$⊢ p = q \to ⟨p, p⟩ = ⟨p, q⟩$
15	14	fveq2d	$⊢ p = q \to D (⟨p, p⟩) = D (⟨p, q⟩)$
16	13 15	eqtrid	$⊢ p = q \to p D p = D (⟨p, q⟩)$
17	12 16	syl	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to p D p = D (⟨p, q⟩)$
18		simplll	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to D \in PsMet (X)$
19	11	simpld	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to p \in X$
20		psmet0	$⊢ (D \in PsMet (X) \land p \in X) \to p D p = 0$
21	18 19 20	syl2anc	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to p D p = 0$
22	17 21	eqtr3d	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to D (⟨p, q⟩) = 0$
23		0xr	$⊢ 0 \in ℝ^{*}$
24		rpxr	$⊢ a \in ℝ^{+} \to a \in ℝ^{*}$
25		rpgt0	$⊢ a \in ℝ^{+} \to 0 < a$
26		lbico1	$⊢ (0 \in ℝ^{} \land a \in ℝ^{} \land 0 < a) \to 0 \in [0, a)$
27	23 24 25 26	mp3an2i	$⊢ a \in ℝ^{+} \to 0 \in [0, a)$
28	27	adantl	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to 0 \in [0, a)$
29	22 28	eqeltrd	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to D (⟨p, q⟩) \in [0, a)$
30		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
31	30	ffund	$⊢ D \in PsMet (X) \to Fun D$
32	31	ad3antrrr	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to Fun D$
33	12 19	eqeltrrd	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to q \in X$
34	19 33	opelxpd	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to ⟨p, q⟩ \in (X \times X)$
35	30	fdmd	$⊢ D \in PsMet (X) \to dom D = X \times X$
36	35	ad3antrrr	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to dom D = X \times X$
37	34 36	eleqtrrd	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to ⟨p, q⟩ \in dom D$
38		fvimacnv	$⊢ (Fun D \land ⟨p, q⟩ \in dom D) \to (D (⟨p, q⟩) \in [0, a) \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
39	32 37 38	syl2anc	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to (D (⟨p, q⟩) \in [0, a) \leftrightarrow ⟨p, q⟩ \in D^{-1} [[0, a)])$
40	29 39	mpbid	$⊢ (((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \to ⟨p, q⟩ \in D^{-1} [[0, a)]$
41	40	adantr	$⊢ ((((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨p, q⟩ \in D^{-1} [[0, a)]$
42		simpr	$⊢ ((((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to A = D^{-1} [[0, a)]$
43	41 42	eleqtrrd	$⊢ ((((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \land a \in ℝ^{+}) \land A = D^{-1} [[0, a)]) \to ⟨p, q⟩ \in A$
44		simplr	$⊢ ((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \to A \in F$
45	1	metustel	$⊢ D \in PsMet (X) \to (A \in F \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
46	45	ad2antrr	$⊢ ((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \to (A \in F \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
47	44 46	mpbid	$⊢ ((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
48	43 47	r19.29a	$⊢ ((D \in PsMet (X) \land A \in F) \land ⟨p, q⟩ \in ({I ↾}_{X})) \to ⟨p, q⟩ \in A$
49	48	ex	$⊢ (D \in PsMet (X) \land A \in F) \to (⟨p, q⟩ \in ({I ↾}_{X}) \to ⟨p, q⟩ \in A)$
50	3 49	relssdv	$⊢ (D \in PsMet (X) \land A \in F) \to {I ↾}_{X} \subseteq A$

Metamath Proof Explorer

Theorem metustid

Proof