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 ‘ 𝑋 ) ∧ 𝐴𝐹𝐵𝐹 ) → ( 𝐴𝐵𝐵𝐴 ) )