Metamath Proof Explorer

Theorem ismet

Description: Express the predicate " D is a metric." (Contributed by NM, 25-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ismet ( 𝑋 ∈ 𝐴 → ( 𝐷 ∈ ( 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-met ⊢ 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 reex ⊢ ℝ ∈ 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 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ) )