This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem restmetu

Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017)

Ref Expression
Assertion restmetu ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( metUnif ‘ 𝐷 ) ↾t ( 𝐴 × 𝐴 ) ) = ( metUnif ‘ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ≠ ∅ )
2 psmetres2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ∈ ( PsMet ‘ 𝐴 ) )
3 2 3adant1 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ∈ ( PsMet ‘ 𝐴 ) )
4 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑏 ) )
5 4 imaeq2d ⊢ ( 𝑎 = 𝑏 → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
6 5 cbvmptv ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) = ( 𝑏 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
7 6 rneqi ⊢ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
8 7 metustfbas ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ∈ ( PsMet ‘ 𝐴 ) ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝐴 × 𝐴 ) ) )
9 1 3 8 syl2anc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝐴 × 𝐴 ) ) )
10 fgval ⊢ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝐴 × 𝐴 ) ) → ( ( 𝐴 × 𝐴 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ) = { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } )
11 9 10 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐴 × 𝐴 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ) = { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } )
12 metuval ⊢ ( ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ∈ ( PsMet ‘ 𝐴 ) → ( metUnif ‘ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ) = ( ( 𝐴 × 𝐴 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ) )
13 3 12 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( metUnif ‘ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ) = ( ( 𝐴 × 𝐴 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ) )
14 fvex ⊢ ( metUnif ‘ 𝐷 ) ∈ V
15 3 elfvexd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
16 15 15 xpexd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) ∈ V )
17 restval ⊢ ( ( ( metUnif ‘ 𝐷 ) ∈ V ∧ ( 𝐴 × 𝐴 ) ∈ V ) → ( ( metUnif ‘ 𝐷 ) ↾t ( 𝐴 × 𝐴 ) ) = ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
18 14 16 17 sylancr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( metUnif ‘ 𝐷 ) ↾t ( 𝐴 × 𝐴 ) ) = ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
19 inss2 ⊢ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
20 sseq1 ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑢 ⊆ ( 𝐴 × 𝐴 ) ↔ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
21 19 20 mpbiri ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → 𝑢 ⊆ ( 𝐴 × 𝐴 ) )
22 vex ⊢ 𝑢 ∈ V
23 22 elpw ⊢ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑢 ⊆ ( 𝐴 × 𝐴 ) )
24 21 23 sylibr ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
25 24 rexlimivw ⊢ ( ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
26 25 adantl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
27 nfv ⊢ Ⅎ 𝑎 ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
28 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
29 28 nfrn ⊢ Ⅎ 𝑎 ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
30 29 nfcri ⊢ Ⅎ 𝑎 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
31 27 30 nfan ⊢ Ⅎ 𝑎 ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
32 nfv ⊢ Ⅎ 𝑎 𝑤 ⊆ 𝑣
33 31 32 nfan ⊢ Ⅎ 𝑎 ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 )
34 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
35 34 nfrn ⊢ Ⅎ 𝑎 ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
36 nfcv ⊢ Ⅎ 𝑎 𝒫 𝑢
37 35 36 nfin ⊢ Ⅎ 𝑎 ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 )
38 nfcv ⊢ Ⅎ 𝑎 ∅
39 37 38 nfne ⊢ Ⅎ 𝑎 ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅
40 simplr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑎 ∈ ℝ+ )
41 ineq1 ⊢ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
42 41 adantl ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
43 simp2 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
44 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
45 ffun ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → Fun 𝐷 )
46 respreima ⊢ ( Fun 𝐷 → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
47 43 44 45 46 4syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
48 47 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
49 42 48 eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
50 rspe ⊢ ( ( 𝑎 ∈ ℝ+ ∧ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) → ∃ 𝑎 ∈ ℝ+ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
51 40 49 50 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ∃ 𝑎 ∈ ℝ+ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
52 vex ⊢ 𝑤 ∈ V
53 52 inex1 ⊢ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ V
54 eqid ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
55 54 elrnmpt ⊢ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) )
56 53 55 ax-mp ⊢ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) )
57 51 56 sylibr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) )
58 simpllr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑤 ⊆ 𝑣 )
59 ssinss1 ⊢ ( 𝑤 ⊆ 𝑣 → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 )
60 58 59 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 )
61 inss2 ⊢ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
62 61 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) )
63 pweq ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → 𝒫 𝑢 = 𝒫 ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
64 63 eleq2d ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 ↔ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
65 53 elpw ⊢ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ↔ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
66 64 65 bitrdi ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 ↔ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
67 ssin ⊢ ( ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 ∧ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) ↔ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
68 66 67 bitr4di ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 ↔ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 ∧ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) ) )
69 68 ad5antlr ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 ↔ ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 ∧ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) ) )
70 60 62 69 mpbir2and ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 )
71 inelcm ⊢ ( ( ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∧ ( 𝑤 ∩ ( 𝐴 × 𝐴 ) ) ∈ 𝒫 𝑢 ) → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ )
72 57 70 71 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) ∧ 𝑎 ∈ ℝ+ ) ∧ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ )
73 simplr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) → 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
74 eqid ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
75 74 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
76 75 elv ⊢ ( 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
77 73 76 sylib ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
78 33 39 72 77 r19.29af2 ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∧ 𝑤 ⊆ 𝑣 ) → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ )
79 ssn0 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≠ ∅ ) → 𝑋 ≠ ∅ )
80 79 ancoms ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ≠ ∅ )
81 80 3adant2 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ≠ ∅ )
82 metuel ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑣 ) ) )
83 81 43 82 syl2anc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑣 ) ) )
84 83 simplbda ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑣 )
85 84 adantr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑣 )
86 78 85 r19.29a ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ )
87 86 r19.29an ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ )
88 26 87 jca ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) )
89 simprl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
90 89 elpwid ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝑢 ⊆ ( 𝐴 × 𝐴 ) )
91 simpl3 ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝐴 ⊆ 𝑋 )
92 xpss12 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
93 91 91 92 syl2anc ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
94 90 93 sstrd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝑢 ⊆ ( 𝑋 × 𝑋 ) )
95 difssd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑋 × 𝑋 ) )
96 94 95 unssd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
97 simplr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → 𝑏 ∈ ℝ+ )
98 eqidd ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
99 4 imaeq2d ⊢ ( 𝑎 = 𝑏 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
100 99 rspceeqv ⊢ ( ( 𝑏 ∈ ℝ+ ∧ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) → ∃ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
101 97 98 100 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ∃ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
102 43 ad4antr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
103 cnvexg ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V )
104 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ V )
105 74 elrnmpt ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ V → ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
106 102 103 104 105 4syl ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
107 101 106 mpbird ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
108 cnvimass ⊢ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ dom 𝐷
109 108 44 fssdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) )
110 102 109 syl ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) )
111 ssdif0 ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑋 × 𝑋 ) ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) = ∅ )
112 110 111 sylib ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) = ∅ )
113 0ss ⊢ ∅ ⊆ 𝑢
114 112 113 eqsstrdi ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) ⊆ 𝑢 )
115 respreima ⊢ ( Fun 𝐷 → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
116 102 44 45 115 4syl ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
117 simpr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
118 simpllr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → 𝑣 ∈ 𝒫 𝑢 )
119 118 elpwid ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → 𝑣 ⊆ 𝑢 )
120 117 119 eqsstrrd ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ⊆ 𝑢 )
121 116 120 eqsstrrd ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑢 )
122 114 121 unssd ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) ∪ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑢 )
123 ssundif ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ 𝑢 ) ⊆ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) )
124 difcom ⊢ ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ 𝑢 ) ⊆ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑢 )
125 difdif2 ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) = ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) ∪ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
126 125 sseq1i ⊢ ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑢 ↔ ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) ∪ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑢 )
127 123 124 126 3bitri ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ↔ ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∖ ( 𝑋 × 𝑋 ) ) ∪ ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑢 )
128 122 127 sylibr ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) )
129 sseq1 ⊢ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) → ( 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ) )
130 129 rspcev ⊢ ( ( ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) )
131 107 128 130 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ∧ 𝑏 ∈ ℝ+ ) ∧ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) )
132 elin ⊢ ( 𝑣 ∈ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ↔ ( 𝑣 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) )
133 6 elrnmpt ⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) )
134 133 elv ⊢ ( 𝑣 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
135 134 anbi1i ⊢ ( ( 𝑣 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ↔ ( ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) )
136 ancom ⊢ ( ( ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) ↔ ( 𝑣 ∈ 𝒫 𝑢 ∧ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) )
137 132 135 136 3bitri ⊢ ( 𝑣 ∈ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ↔ ( 𝑣 ∈ 𝒫 𝑢 ∧ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) )
138 137 exbii ⊢ ( ∃ 𝑣 𝑣 ∈ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝒫 𝑢 ∧ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) )
139 n0 ⊢ ( ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) )
140 df-rex ⊢ ( ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝒫 𝑢 ∧ ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) ) )
141 138 139 140 3bitr4i ⊢ ( ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
142 141 biimpi ⊢ ( ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ → ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
143 142 ad2antll ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ ℝ+ 𝑣 = ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑏 ) ) )
144 131 143 r19.29vva ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) )
145 81 adantr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝑋 ≠ ∅ )
146 43 adantr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
147 metuel ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∈ ( metUnif ‘ 𝐷 ) ↔ ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ) ) )
148 145 146 147 syl2anc ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∈ ( metUnif ‘ 𝐷 ) ↔ ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ) ) )
149 96 144 148 mpbir2and ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∈ ( metUnif ‘ 𝐷 ) )
150 indir ⊢ ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∪ ( ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ∩ ( 𝐴 × 𝐴 ) ) )
151 disjdifr ⊢ ( ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ∅
152 151 uneq2i ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∪ ( ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∪ ∅ )
153 un0 ⊢ ( ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) ∪ ∅ ) = ( 𝑢 ∩ ( 𝐴 × 𝐴 ) )
154 150 152 153 3eqtri ⊢ ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝑢 ∩ ( 𝐴 × 𝐴 ) )
155 dfss2 ⊢ ( 𝑢 ⊆ ( 𝐴 × 𝐴 ) ↔ ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) = 𝑢 )
156 90 155 sylib ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐴 ) ) = 𝑢 )
157 154 156 eqtr2id ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → 𝑢 = ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∩ ( 𝐴 × 𝐴 ) ) )
158 ineq1 ⊢ ( 𝑣 = ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) → ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∩ ( 𝐴 × 𝐴 ) ) )
159 158 rspceeqv ⊢ ( ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑢 = ( ( 𝑢 ∪ ( ( 𝑋 × 𝑋 ) ∖ ( 𝐴 × 𝐴 ) ) ) ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
160 149 157 159 syl2anc ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
161 88 160 impbida ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ↔ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) ) )
162 eqid ⊢ ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) = ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
163 162 elrnmpt ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
164 163 elv ⊢ ( 𝑢 ∈ ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
165 pweq ⊢ ( 𝑣 = 𝑢 → 𝒫 𝑣 = 𝒫 𝑢 )
166 165 ineq2d ⊢ ( 𝑣 = 𝑢 → ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) = ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) )
167 166 neeq1d ⊢ ( 𝑣 = 𝑢 → ( ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ ↔ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) )
168 167 elrab ⊢ ( 𝑢 ∈ { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } ↔ ( 𝑢 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∧ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑢 ) ≠ ∅ ) )
169 161 164 168 3bitr4g ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑢 ∈ ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ 𝑢 ∈ { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } ) )
170 169 eqrdv ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ran ( 𝑣 ∈ ( metUnif ‘ 𝐷 ) ↦ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) = { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } )
171 18 170 eqtrd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( metUnif ‘ 𝐷 ) ↾t ( 𝐴 × 𝐴 ) ) = { 𝑣 ∈ 𝒫 ( 𝐴 × 𝐴 ) ∣ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) “ ( 0 [,) 𝑎 ) ) ) ∩ 𝒫 𝑣 ) ≠ ∅ } )
172 11 13 171 3eqtr4rd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( metUnif ‘ 𝐷 ) ↾t ( 𝐴 × 𝐴 ) ) = ( metUnif ‘ ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) ) )