Metamath Proof Explorer


Theorem isxmet

Description: Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion isxmet ( 𝑋𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ( 𝑋𝐴𝑋 ∈ V )
2 xpeq12 ( ( 𝑡 = 𝑋𝑡 = 𝑋 ) → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
3 2 anidms ( 𝑡 = 𝑋 → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
4 3 oveq2d ( 𝑡 = 𝑋 → ( ℝ*m ( 𝑡 × 𝑡 ) ) = ( ℝ*m ( 𝑋 × 𝑋 ) ) )
5 raleq ( 𝑡 = 𝑋 → ( ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) )
6 5 anbi2d ( 𝑡 = 𝑋 → ( ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
7 6 raleqbi1dv ( 𝑡 = 𝑋 → ( ∀ 𝑦𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
8 7 raleqbi1dv ( 𝑡 = 𝑋 → ( ∀ 𝑥𝑡𝑦𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ) )
9 4 8 rabeqbidv ( 𝑡 = 𝑋 → { 𝑑 ∈ ( ℝ*m ( 𝑡 × 𝑡 ) ) ∣ ∀ 𝑥𝑡𝑦𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
10 df-xmet ∞Met = ( 𝑡 ∈ V ↦ { 𝑑 ∈ ( ℝ*m ( 𝑡 × 𝑡 ) ) ∣ ∀ 𝑥𝑡𝑦𝑡 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑡 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
11 ovex ( ℝ*m ( 𝑋 × 𝑋 ) ) ∈ V
12 11 rabex { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ∈ V
13 9 10 12 fvmpt ( 𝑋 ∈ V → ( ∞Met ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
14 1 13 syl ( 𝑋𝐴 → ( ∞Met ‘ 𝑋 ) = { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } )
15 14 eleq2d ( 𝑋𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ 𝐷 ∈ { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ) )
16 oveq ( 𝑑 = 𝐷 → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
17 16 eqeq1d ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑦 ) = 0 ) )
18 17 bibi1d ( 𝑑 = 𝐷 → ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ) )
19 oveq ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑥 ) = ( 𝑧 𝐷 𝑥 ) )
20 oveq ( 𝑑 = 𝐷 → ( 𝑧 𝑑 𝑦 ) = ( 𝑧 𝐷 𝑦 ) )
21 19 20 oveq12d ( 𝑑 = 𝐷 → ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
22 16 21 breq12d ( 𝑑 = 𝐷 → ( ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
23 22 ralbidv ( 𝑑 = 𝐷 → ( ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ↔ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
24 18 23 anbi12d ( 𝑑 = 𝐷 → ( ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
25 24 2ralbidv ( 𝑑 = 𝐷 → ( ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
26 25 elrab ( 𝐷 ∈ { 𝑑 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝑑 𝑦 ) ≤ ( ( 𝑧 𝑑 𝑥 ) +𝑒 ( 𝑧 𝑑 𝑦 ) ) ) } ↔ ( 𝐷 ∈ ( ℝ*m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
27 15 26 bitrdi ( 𝑋𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ℝ*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 ( 𝑋𝐴 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )