Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion metustto ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 simpll ⊢ ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → 𝑎 ∈ ℝ+ )
3 2 rpred ⊢ ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → 𝑎 ∈ ℝ )
4 simplr ⊢ ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → 𝑏 ∈ ℝ+ )
5 4 rpred ⊢ ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → 𝑏 ∈ ℝ )
6 simpllr ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ℝ+ )
7 6 rpred ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ℝ )
8 0xr ⊢ 0 ∈ ℝ*
9 8 a1i ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → 0 ∈ ℝ* )
10 simpl ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ℝ )
11 10 rexrd ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ℝ* )
12 0le0 ⊢ 0 ≤ 0
13 12 a1i ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → 0 ≤ 0 )
14 simpr ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → 𝑎 ≤ 𝑏 )
15 icossico ⊢ ( ( ( 0 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 𝑎 ≤ 𝑏 ) ) → ( 0 [,) 𝑎 ) ⊆ ( 0 [,) 𝑏 ) )
16 9 11 13 14 15 syl22anc ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → ( 0 [,) 𝑎 ) ⊆ ( 0 [,) 𝑏 ) )
17 imass2 ⊢ ( ( 0 [,) 𝑎 ) ⊆ ( 0 [,) 𝑏 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
18 16 17 syl ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
19 7 18 sylancom ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
20 simplrl ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
21 simplrr ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
22 19 20 21 3sstr4d ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → 𝐴 ⊆ 𝐵 )
23 22 orcd ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑎 ≤ 𝑏 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
24 simplll ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ℝ+ )
25 24 rpred ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ℝ )
26 8 a1i ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → 0 ∈ ℝ* )
27 simpl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ℝ )
28 27 rexrd ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → 𝑎 ∈ ℝ* )
29 12 a1i ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → 0 ≤ 0 )
30 simpr ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → 𝑏 ≤ 𝑎 )
31 icossico ⊢ ( ( ( 0 ∈ ℝ* ∧ 𝑎 ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 𝑏 ≤ 𝑎 ) ) → ( 0 [,) 𝑏 ) ⊆ ( 0 [,) 𝑎 ) )
32 26 28 29 30 31 syl22anc ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → ( 0 [,) 𝑏 ) ⊆ ( 0 [,) 𝑎 ) )
33 imass2 ⊢ ( ( 0 [,) 𝑏 ) ⊆ ( 0 [,) 𝑎 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
34 32 33 syl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ≤ 𝑎 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
35 25 34 sylancom ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
36 simplrr ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
37 simplrl ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
38 35 36 37 3sstr4d ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → 𝐵 ⊆ 𝐴 )
39 38 olcd ⊢ ( ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∧ 𝑏 ≤ 𝑎 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
40 3 5 23 39 lecasei ⊢ ( ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
41 40 adantlll ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
42 1 metustel ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
43 42 biimpa ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
44 43 3adant3 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
45 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑏 ) )
46 45 imaeq2d ⊢ ( 𝑎 = 𝑏 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
47 46 cbvmptv ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
48 47 rneqi ⊢ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
49 1 48 eqtri ⊢ 𝐹 = ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
50 49 metustel ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ 𝐹 ↔ ∃ 𝑏 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
51 50 biimpa ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑏 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
52 51 3adant2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑏 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
53 reeanv ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ( ∃ 𝑎 ∈ ℝ+ 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ∃ 𝑏 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
54 44 52 53 sylanbrc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( 𝐴 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
55 41 54 r19.29vva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )