Metamath Proof Explorer

Theorem metf1o

Description: Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis metf1o.2 ⊢ 𝑁 = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑌 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) )
Assertion metf1o ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 metf1o.2 ⊢ 𝑁 = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑌 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) )
2 f1of ⊢ ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 → 𝐹 : 𝑌 ⟶ 𝑋 )
3 ffvelcdm ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
4 3 ex ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑥 ∈ 𝑌 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) )
5 ffvelcdm ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 )
6 5 ex ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑦 ∈ 𝑌 → ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) )
7 4 6 anim12d ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) ) )
8 2 7 syl ⊢ ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) ) )
9 metcl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
10 9 3expib ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) )
11 8 10 sylan9r ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) )
12 11 3adant1 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) )
13 12 ralrimivv ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
14 1 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ↔ 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ )
15 13 14 sylib ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ )
16 fveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) )
17 16 oveq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) )
18 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑣 ) )
19 18 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
20 ovex ⊢ ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ∈ V
21 17 19 1 20 ovmpo ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( 𝑢 𝑁 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
22 21 eqeq1d ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ) )
23 22 adantl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ) )
24 ffvelcdm ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑢 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 )
25 24 ex ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑢 ∈ 𝑌 → ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) )
26 ffvelcdm ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 )
27 26 ex ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑣 ∈ 𝑌 → ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) )
28 25 27 anim12d ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) )
29 2 28 syl ⊢ ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) )
30 29 imp ⊢ ( ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) )
31 30 adantll ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) )
32 meteq0 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) )
33 32 3expb ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) )
34 33 adantlr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) )
35 31 34 syldan ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) = 0 ↔ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) )
36 f1of1 ⊢ ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 → 𝐹 : 𝑌 –1-1→ 𝑋 )
37 f1fveq ⊢ ( ( 𝐹 : 𝑌 –1-1→ 𝑋 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 = 𝑣 ) )
38 36 37 sylan ⊢ ( ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 = 𝑣 ) )
39 38 adantll ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ 𝑢 = 𝑣 ) )
40 23 35 39 3bitrd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) )
41 ffvelcdm ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑤 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 )
42 41 ex ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑤 ∈ 𝑌 → ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) )
43 28 42 anim12d ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) ) )
44 2 43 syl ⊢ ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) ) )
45 44 imp ⊢ ( ( 𝐹 : 𝑌 –1-1-onto→ 𝑋 ∧ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) )
46 45 adantll ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) )
47 mettri2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
48 47 expcom ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) → ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) ) )
49 48 3expb ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ) → ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) ) )
50 49 ancoms ⊢ ( ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) → ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) ) )
51 50 impcom ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
52 51 adantlr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
53 46 52 syldan ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
54 53 anassrs ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
55 21 adantr ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑢 𝑁 𝑣 ) = ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
56 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
57 56 oveq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) )
58 fveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑢 ) )
59 58 oveq2d ⊢ ( 𝑦 = 𝑢 → ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) )
60 ovex ⊢ ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) ∈ V
61 57 59 1 60 ovmpo ⊢ ( ( 𝑤 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑢 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) )
62 61 ancoms ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑢 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) )
63 62 adantlr ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑢 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) )
64 18 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
65 ovex ⊢ ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ∈ V
66 57 64 1 65 ovmpo ⊢ ( ( 𝑤 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑣 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
67 66 ancoms ⊢ ( ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑣 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
68 67 adantll ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 𝑁 𝑣 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) )
69 63 68 oveq12d ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) )
70 55 69 breq12d ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) ) )
71 70 adantll ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑢 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ≤ ( ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑢 ) ) + ( ( 𝐹 ‘ 𝑤 ) 𝑀 ( 𝐹 ‘ 𝑣 ) ) ) ) )
72 54 71 mpbird ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) )
73 72 ralrimiva ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) )
74 40 73 jca ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) )
75 74 3adantl1 ⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) ∧ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) )
76 75 ex ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) ) )
77 76 ralrimivv ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) )
78 ismet ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑁 ∈ ( Met ‘ 𝑌 ) ↔ ( 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) ) ) )
79 78 3ad2ant1 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → ( 𝑁 ∈ ( Met ‘ 𝑌 ) ↔ ( 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ ∧ ∀ 𝑢 ∈ 𝑌 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑢 𝑁 𝑣 ) = 0 ↔ 𝑢 = 𝑣 ) ∧ ∀ 𝑤 ∈ 𝑌 ( 𝑢 𝑁 𝑣 ) ≤ ( ( 𝑤 𝑁 𝑢 ) + ( 𝑤 𝑁 𝑣 ) ) ) ) ) )
80 15 77 79 mpbir2and ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )