Metamath Proof Explorer

Theorem metuel2

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metuel2.u ⊢ 𝑈 = ( metUnif ‘ 𝐷 )
Assertion metuel2 ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ 𝑈 ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 metuel2.u ⊢ 𝑈 = ( metUnif ‘ 𝐷 )
2 1 eleq2i ⊢ ( 𝑉 ∈ 𝑈 ↔ 𝑉 ∈ ( metUnif ‘ 𝐷 ) )
3 2 a1i ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ 𝑈 ↔ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ) )
4 metuel ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) )
5 oveq2 ⊢ ( 𝑎 = 𝑑 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑑 ) )
6 5 imaeq2d ⊢ ( 𝑎 = 𝑑 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
7 6 cbvmptv ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
8 7 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑑 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) )
9 8 elv ⊢ ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑑 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
10 9 anbi1i ⊢ ( ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ( ∃ 𝑑 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
11 r19.41v ⊢ ( ∃ 𝑑 ∈ ℝ+ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ( ∃ 𝑑 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
12 10 11 bitr4i ⊢ ( ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ∃ 𝑑 ∈ ℝ+ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
13 12 exbii ⊢ ( ∃ 𝑤 ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ∃ 𝑤 ∃ 𝑑 ∈ ℝ+ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
14 df-rex ⊢ ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ↔ ∃ 𝑤 ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑤 ⊆ 𝑉 ) )
15 rexcom4 ⊢ ( ∃ 𝑑 ∈ ℝ+ ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ∃ 𝑤 ∃ 𝑑 ∈ ℝ+ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
16 13 14 15 3bitr4i ⊢ ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ↔ ∃ 𝑑 ∈ ℝ+ ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) )
17 cnvexg ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V )
18 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V )
19 sseq1 ⊢ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ( 𝑤 ⊆ 𝑉 ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
20 19 ceqsexgv ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V → ( ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
21 17 18 20 3syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
22 21 rexbidv ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ℝ+ ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ∃ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
23 22 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑑 ∈ ℝ+ ∃ 𝑤 ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∧ 𝑤 ⊆ 𝑉 ) ↔ ∃ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
24 16 23 syl5bb ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ↔ ∃ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ) )
25 cnvimass ⊢ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ dom 𝐷
26 simpll ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
27 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
28 fdm ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
29 26 27 28 3syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
30 25 29 sseqtrid ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ ( 𝑋 × 𝑋 ) )
31 ssrel2 ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ ( 𝑋 × 𝑋 ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 ) ) )
32 30 31 syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 ) ) )
33 simplr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
34 simpr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
35 33 34 opelxpd ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) )
36 35 biantrurd ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) ) ) )
37 psmetcl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
38 37 ad5ant145 ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
39 38 3biant1d ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ↔ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ) )
40 psmetge0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
41 40 biantrurd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ( 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ) )
42 41 ad5ant145 ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ( 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ) )
43 0xr ⊢ 0 ∈ ℝ*
44 simpllr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑑 ∈ ℝ+ )
45 44 rpxrd ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑑 ∈ ℝ* )
46 elico1 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑑 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,) 𝑑 ) ↔ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ) )
47 43 45 46 sylancr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,) 𝑑 ) ↔ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ∧ ( 𝑥 𝐷 𝑦 ) < 𝑑 ) ) )
48 39 42 47 3bitr4d ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,) 𝑑 ) ) )
49 df-ov ⊢ ( 𝑥 𝐷 𝑦 ) = ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
50 49 eleq1i ⊢ ( ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,) 𝑑 ) ↔ ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) )
51 48 50 bitrdi ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) ) )
52 simp-4l ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
53 ffn ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝐷 Fn ( 𝑋 × 𝑋 ) )
54 elpreima ⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) ) ) )
55 52 27 53 54 4syl ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( 0 [,) 𝑑 ) ) ) )
56 36 51 55 3bitr4d ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) )
57 56 anasss ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) < 𝑑 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) )
58 df-br ⊢ ( 𝑥 𝑉 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 )
59 58 a1i ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑉 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 ) )
60 57 59 imbi12d ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 ) ) )
61 60 2ralbidva ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑉 ) ) )
62 32 61 bitr4d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑑 ∈ ℝ+ ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) )
63 62 rexbidva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ⊆ 𝑉 ↔ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) )
64 24 63 bitrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ⊆ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ↔ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) )
65 64 pm5.32da ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) ) )
66 65 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) ) )
67 3 4 66 3bitrd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ 𝑈 ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → 𝑥 𝑉 𝑦 ) ) ) )