Metamath Proof Explorer


Theorem metustsym

Description: Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion metustsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → 𝐴 = 𝐴 )

Proof

Step Hyp Ref Expression
1 metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 1 metustss ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) )
3 cnvss ( 𝐴 ⊆ ( 𝑋 × 𝑋 ) → 𝐴 ( 𝑋 × 𝑋 ) )
4 cnvxp ( 𝑋 × 𝑋 ) = ( 𝑋 × 𝑋 )
5 3 4 sseqtrdi ( 𝐴 ⊆ ( 𝑋 × 𝑋 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) )
6 2 5 syl ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) )
7 simp-4l ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
8 simpr1r ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( ( 𝑝𝑋𝑞𝑋 ) ∧ 𝑎 ∈ ℝ+𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) → 𝑞𝑋 )
9 8 3anassrs ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑞𝑋 )
10 simpr1l ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( ( 𝑝𝑋𝑞𝑋 ) ∧ 𝑎 ∈ ℝ+𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) → 𝑝𝑋 )
11 10 3anassrs ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑝𝑋 )
12 psmetsym ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑞𝑋𝑝𝑋 ) → ( 𝑞 𝐷 𝑝 ) = ( 𝑝 𝐷 𝑞 ) )
13 7 9 11 12 syl3anc ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑞 𝐷 𝑝 ) = ( 𝑝 𝐷 𝑞 ) )
14 df-ov ( 𝑞 𝐷 𝑝 ) = ( 𝐷 ‘ ⟨ 𝑞 , 𝑝 ⟩ )
15 df-ov ( 𝑝 𝐷 𝑞 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ )
16 13 14 15 3eqtr3g ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝐷 ‘ ⟨ 𝑞 , 𝑝 ⟩ ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
17 16 eleq1d ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( 𝐷 ‘ ⟨ 𝑞 , 𝑝 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ) )
18 psmetf ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
19 ffun ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → Fun 𝐷 )
20 7 18 19 3syl ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → Fun 𝐷 )
21 simpllr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑝𝑋𝑞𝑋 ) )
22 21 ancomd ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑞𝑋𝑝𝑋 ) )
23 opelxpi ( ( 𝑞𝑋𝑝𝑋 ) → ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝑋 × 𝑋 ) )
24 22 23 syl ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝑋 × 𝑋 ) )
25 fdm ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
26 7 18 25 3syl ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
27 24 26 eleqtrrd ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑞 , 𝑝 ⟩ ∈ dom 𝐷 )
28 fvimacnv ( ( Fun 𝐷 ∧ ⟨ 𝑞 , 𝑝 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑞 , 𝑝 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
29 20 27 28 syl2anc ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( 𝐷 ‘ ⟨ 𝑞 , 𝑝 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
30 opelxpi ( ( 𝑝𝑋𝑞𝑋 ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
31 21 30 syl ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
32 31 26 eleqtrrd ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 )
33 fvimacnv ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
34 20 32 33 syl2anc ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
35 17 29 34 3bitr3d ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
36 simpr ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
37 36 eleq2d ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ⟨ 𝑞 , 𝑝 ⟩ ∈ 𝐴 ↔ ⟨ 𝑞 , 𝑝 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
38 36 eleq2d ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
39 35 37 38 3bitr4d ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ⟨ 𝑞 , 𝑝 ⟩ ∈ 𝐴 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ) )
40 eqid ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
41 40 elrnmpt ( 𝐴 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝐴 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
42 41 ibi ( 𝐴 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
43 42 1 eleq2s ( 𝐴𝐹 → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
44 43 ad2antlr ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) → ∃ 𝑎 ∈ ℝ+ 𝐴 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
45 39 44 r19.29a ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) → ( ⟨ 𝑞 , 𝑝 ⟩ ∈ 𝐴 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ) )
46 df-br ( 𝑝 𝐴 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
47 vex 𝑝 ∈ V
48 vex 𝑞 ∈ V
49 47 48 opelcnv ( ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ↔ ⟨ 𝑞 , 𝑝 ⟩ ∈ 𝐴 )
50 46 49 bitri ( 𝑝 𝐴 𝑞 ↔ ⟨ 𝑞 , 𝑝 ⟩ ∈ 𝐴 )
51 df-br ( 𝑝 𝐴 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
52 45 50 51 3bitr4g ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ ( 𝑝𝑋𝑞𝑋 ) ) → ( 𝑝 𝐴 𝑞𝑝 𝐴 𝑞 ) )
53 52 3impb ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) ∧ 𝑝𝑋𝑞𝑋 ) → ( 𝑝 𝐴 𝑞𝑝 𝐴 𝑞 ) )
54 6 2 53 eqbrrdva ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴𝐹 ) → 𝐴 = 𝐴 )