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 ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ◡ 𝐴 = 𝐴 )