Metamath Proof Explorer

Theorem ispsmet

Description: Express the predicate " D is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion ispsmet ( 𝑋 ∈ 𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
2 id ⊢ ( 𝑢 = 𝑋 → 𝑢 = 𝑋 )
3 2 sqxpeqd ⊢ ( 𝑢 = 𝑋 → ( 𝑢 × 𝑢 ) = ( 𝑋 × 𝑋 ) )
4 3 oveq2d ⊢ ( 𝑢 = 𝑋 → ( ℝ* ↑m ( 𝑢 × 𝑢 ) ) = ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) )
5 raleq ⊢ ( 𝑢 = 𝑋 → ( ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
6 5 raleqbi1dv ⊢ ( 𝑢 = 𝑋 → ( ∀ 𝑦 ∈ 𝑢 ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
7 6 anbi2d ⊢ ( 𝑢 = 𝑋 → ( ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑢 ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
8 7 raleqbi1dv ⊢ ( 𝑢 = 𝑋 → ( ∀ 𝑥 ∈ 𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑢 ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
9 4 8 rabeqbidv ⊢ ( 𝑢 = 𝑋 → { 𝑑 ∈ ( ℝ* ↑m ( 𝑢 × 𝑢 ) ) ∣ ∀ 𝑥 ∈ 𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑢 ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
10 df-psmet ⊢ PsMet = ( 𝑢 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑢 × 𝑢 ) ) ∣ ∀ 𝑥 ∈ 𝑢 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑢 ∀ 𝑧 ∈ 𝑢 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
11 ovex ⊢ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∈ V
12 11 rabex ⊢ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ∈ V
13 9 10 12 fvmpt ⊢ ( 𝑋 ∈ V → ( PsMet ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
14 1 13 syl ⊢ ( 𝑋 ∈ 𝑉 → ( PsMet ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
15 14 eleq2d ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ 𝐷 ∈ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ) )
16 oveq ⊢ ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑥 ) = ( 𝑥 𝐷 𝑥 ) )
17 16 eqeq1d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑥 ) = 0 ↔ ( 𝑥 𝐷 𝑥 ) = 0 ) )
18 oveq ⊢ ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
19 oveq ⊢ ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑥 ) = ( 𝑧 𝐷 𝑥 ) )
20 oveq ⊢ ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑦 ) = ( 𝑧 𝐷 𝑦 ) )
21 19 20 oveq12d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
22 18 21 breq12d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
23 22 2ralbidv ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
24 17 23 anbi12d ⊢ ( 𝑑 = 𝐷 → ( ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
25 24 ralbidv ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
26 25 elrab ⊢ ( 𝐷 ∈ { 𝑑 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝑑 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ↔ ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
27 15 26 bitrdi ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
28 xrex ⊢ ℝ* ∈ V
29 sqxpexg ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 × 𝑋 ) ∈ V )
30 elmapg ⊢ ( ( ℝ* ∈ V ∧ ( 𝑋 × 𝑋 ) ∈ V ) → ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
31 28 29 30 sylancr ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ↔ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ) )
32 31 anbi1d ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐷 ∈ ( ℝ* ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
33 27 32 bitrd ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )