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 ↾ 𝑋 ) ⊆ 𝐴 )