Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 relres Rel ( I ↾ 𝑋 )
3 2 a1i ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → Rel ( I ↾ 𝑋 ) )
4 vex 𝑞 ∈ V
5 4 brresi ( 𝑝 ( I ↾ 𝑋 ) 𝑞 ↔ ( 𝑝𝑋𝑝 I 𝑞 ) )
6 df-br ( 𝑝 ( I ↾ 𝑋 ) 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) )
7 4 ideq ( 𝑝 I 𝑞𝑝 = 𝑞 )
8 7 anbi2i ( ( 𝑝𝑋𝑝 I 𝑞 ) ↔ ( 𝑝𝑋𝑝 = 𝑞 ) )
9 5 6 8 3bitr3i ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ↔ ( 𝑝𝑋𝑝 = 𝑞 ) )
10 9 biimpi ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) → ( 𝑝𝑋𝑝 = 𝑞 ) )
11 10 ad2antlr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( 𝑝𝑋𝑝 = 𝑞 ) )
12 11 simprd ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → 𝑝 = 𝑞 )
13 df-ov ( 𝑝 𝐷 𝑝 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑝 ⟩ )
14 opeq2 ( 𝑝 = 𝑞 → ⟨ 𝑝 , 𝑝 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ )
15 14 fveq2d ( 𝑝 = 𝑞 → ( 𝐷 ‘ ⟨ 𝑝 , 𝑝 ⟩ ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
16 13 15 syl5eq ( 𝑝 = 𝑞 → ( 𝑝 𝐷 𝑝 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
17 12 16 syl ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( 𝑝 𝐷 𝑝 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
18 simplll ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
19 11 simpld ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → 𝑝𝑋 )
20 psmet0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( 𝑝 𝐷 𝑝 ) = 0 )
21 18 19 20 syl2anc ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( 𝑝 𝐷 𝑝 ) = 0 )
22 17 21 eqtr3d ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) = 0 )
23 0xr 0 ∈ ℝ*
24 rpxr ( 𝑎 ∈ ℝ+𝑎 ∈ ℝ* )
25 rpgt0 ( 𝑎 ∈ ℝ+ → 0 < 𝑎 )
26 lbico1 ( ( 0 ∈ ℝ*𝑎 ∈ ℝ* ∧ 0 < 𝑎 ) → 0 ∈ ( 0 [,) 𝑎 ) )
27 23 24 25 26 mp3an2i ( 𝑎 ∈ ℝ+ → 0 ∈ ( 0 [,) 𝑎 ) )
28 27 adantl ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → 0 ∈ ( 0 [,) 𝑎 ) )
29 22 28 eqeltrd ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) )
30 psmetf ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
31 30 ffund ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → Fun 𝐷 )
32 31 ad3antrrr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → Fun 𝐷 )
33 12 19 eqeltrrd ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → 𝑞𝑋 )
34 19 33 opelxpd ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
35 30 fdmd ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
36 35 ad3antrrr ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
37 34 36 eleqtrrd ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 )
38 fvimacnv ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
39 32 37 38 syl2anc ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
40 29 39 mpbid ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
41 40 adantr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
42 simpr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
43 41 42 eleqtrrd ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
44 simplr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) → 𝐴𝐹 )
45 1 metustel ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐴𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
46 45 ad2antrr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) → ( 𝐴𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
47 44 46 mpbid ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
48 43 47 r19.29a ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
49 48 ex ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( I ↾ 𝑋 ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ) )
50 3 49 relssdv ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝐴 )