metustto

Description: Any two elements of the filter base generated by the metric D can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustto	$⊢ (D \in PsMet (X) \land A \in F \land B \in F) \to (A \subseteq B \lor B \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2		simpll	$⊢ ((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to a \in ℝ^{+}$
3	2	rpred	$⊢ ((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to a \in ℝ$
4		simplr	$⊢ ((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to b \in ℝ^{+}$
5	4	rpred	$⊢ ((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to b \in ℝ$
6		simpllr	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to b \in ℝ^{+}$
7	6	rpred	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to b \in ℝ$
8		0xr	$⊢ 0 \in ℝ^{*}$
9	8	a1i	$⊢ (b \in ℝ \land a \leq b) \to 0 \in ℝ^{*}$
10		simpl	$⊢ (b \in ℝ \land a \leq b) \to b \in ℝ$
11	10	rexrd	$⊢ (b \in ℝ \land a \leq b) \to b \in ℝ^{*}$
12		0le0	$⊢ 0 \leq 0$
13	12	a1i	$⊢ (b \in ℝ \land a \leq b) \to 0 \leq 0$
14		simpr	$⊢ (b \in ℝ \land a \leq b) \to a \leq b$
15		icossico	$⊢ ((0 \in ℝ^{} \land b \in ℝ^{}) \land (0 \leq 0 \land a \leq b)) \to [0, a) \subseteq [0, b)$
16	9 11 13 14 15	syl22anc	$⊢ (b \in ℝ \land a \leq b) \to [0, a) \subseteq [0, b)$
17		imass2	$⊢ [0, a) \subseteq [0, b) \to D^{-1} [[0, a)] \subseteq D^{-1} [[0, b)]$
18	16 17	syl	$⊢ (b \in ℝ \land a \leq b) \to D^{-1} [[0, a)] \subseteq D^{-1} [[0, b)]$
19	7 18	sylancom	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to D^{-1} [[0, a)] \subseteq D^{-1} [[0, b)]$
20		simplrl	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to A = D^{-1} [[0, a)]$
21		simplrr	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to B = D^{-1} [[0, b)]$
22	19 20 21	3sstr4d	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to A \subseteq B$
23	22	orcd	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land a \leq b) \to (A \subseteq B \lor B \subseteq A)$
24		simplll	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to a \in ℝ^{+}$
25	24	rpred	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to a \in ℝ$
26	8	a1i	$⊢ (a \in ℝ \land b \leq a) \to 0 \in ℝ^{*}$
27		simpl	$⊢ (a \in ℝ \land b \leq a) \to a \in ℝ$
28	27	rexrd	$⊢ (a \in ℝ \land b \leq a) \to a \in ℝ^{*}$
29	12	a1i	$⊢ (a \in ℝ \land b \leq a) \to 0 \leq 0$
30		simpr	$⊢ (a \in ℝ \land b \leq a) \to b \leq a$
31		icossico	$⊢ ((0 \in ℝ^{} \land a \in ℝ^{}) \land (0 \leq 0 \land b \leq a)) \to [0, b) \subseteq [0, a)$
32	26 28 29 30 31	syl22anc	$⊢ (a \in ℝ \land b \leq a) \to [0, b) \subseteq [0, a)$
33		imass2	$⊢ [0, b) \subseteq [0, a) \to D^{-1} [[0, b)] \subseteq D^{-1} [[0, a)]$
34	32 33	syl	$⊢ (a \in ℝ \land b \leq a) \to D^{-1} [[0, b)] \subseteq D^{-1} [[0, a)]$
35	25 34	sylancom	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to D^{-1} [[0, b)] \subseteq D^{-1} [[0, a)]$
36		simplrr	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to B = D^{-1} [[0, b)]$
37		simplrl	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to A = D^{-1} [[0, a)]$
38	35 36 37	3sstr4d	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to B \subseteq A$
39	38	olcd	$⊢ (((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \land b \leq a) \to (A \subseteq B \lor B \subseteq A)$
40	3 5 23 39	lecasei	$⊢ ((a \in ℝ^{+} \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to (A \subseteq B \lor B \subseteq A)$
41	40	adantlll	$⊢ ((((D \in PsMet (X) \land A \in F \land B \in F) \land a \in ℝ^{+}) \land b \in ℝ^{+}) \land (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])) \to (A \subseteq B \lor B \subseteq A)$
42	1	metustel	$⊢ D \in PsMet (X) \to (A \in F \leftrightarrow \exists a \in ℝ^{+} A = D^{-1} [[0, a)])$
43	42	biimpa	$⊢ (D \in PsMet (X) \land A \in F) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
44	43	3adant3	$⊢ (D \in PsMet (X) \land A \in F \land B \in F) \to \exists a \in ℝ^{+} A = D^{-1} [[0, a)]$
45		oveq2	$⊢ a = b \to [0, a) = [0, b)$
46	45	imaeq2d	$⊢ a = b \to D^{-1} [[0, a)] = D^{-1} [[0, b)]$
47	46	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
48	47	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
49	1 48	eqtri	$⊢ F = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
50	49	metustel	$⊢ D \in PsMet (X) \to (B \in F \leftrightarrow \exists b \in ℝ^{+} B = D^{-1} [[0, b)])$
51	50	biimpa	$⊢ (D \in PsMet (X) \land B \in F) \to \exists b \in ℝ^{+} B = D^{-1} [[0, b)]$
52	51	3adant2	$⊢ (D \in PsMet (X) \land A \in F \land B \in F) \to \exists b \in ℝ^{+} B = D^{-1} [[0, b)]$
53		reeanv	$⊢ \exists a \in ℝ^{+} \exists b \in ℝ^{+} (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)]) \leftrightarrow (\exists a \in ℝ^{+} A = D^{-1} [[0, a)] \land \exists b \in ℝ^{+} B = D^{-1} [[0, b)])$
54	44 52 53	sylanbrc	$⊢ (D \in PsMet (X) \land A \in F \land B \in F) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} (A = D^{-1} [[0, a)] \land B = D^{-1} [[0, b)])$
55	41 54	r19.29vva	$⊢ (D \in PsMet (X) \land A \in F \land B \in F) \to (A \subseteq B \lor B \subseteq A)$

Metamath Proof Explorer

Theorem metustto

Proof