Metamath Proof Explorer

Theorem imasf1oxmet

Description: The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasf1oxmet.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasf1oxmet.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasf1oxmet.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasf1oxmet.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
imasf1oxmet.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
imasf1oxmet.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
Assertion imasf1oxmet ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasf1oxmet.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasf1oxmet.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasf1oxmet.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasf1oxmet.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 imasf1oxmet.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
7 imasf1oxmet.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
8 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
9 3 8 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
10 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
11 1 2 9 4 10 6 imasdsfn ⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
14 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
15 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑅 ∈ 𝑍 )
16 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
19 12 13 14 15 5 6 16 17 18 imasdsf1o ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐸 𝑏 ) )
20 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ* )
21 20 3expb ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ* )
22 7 21 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ∈ ℝ* )
23 19 22 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* )
24 23 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* )
25 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 Fn 𝑉 )
26 3 25 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
27 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) )
28 27 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* ) )
29 28 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* ) )
30 26 29 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* ) )
31 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
32 9 31 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
33 32 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
34 30 33 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
35 34 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ* ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
36 24 35 mpbid ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* )
37 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) )
38 37 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
39 38 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
40 39 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
41 26 40 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ) )
42 32 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ) )
43 41 42 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ∈ ℝ* ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ) )
44 36 43 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
45 ffnov ⊢ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* ↔ ( 𝐷 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ) )
46 11 44 45 sylanbrc ⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* )
47 xmeteq0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 𝐸 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
48 16 17 18 47 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑎 𝐸 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
49 19 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝑎 𝐸 𝑏 ) = 0 ) )
50 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –1-1→ 𝐵 )
51 3 50 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1→ 𝐵 )
52 f1fveq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
53 51 52 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
54 48 49 53 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
55 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
56 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
57 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
58 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
59 xmettri2 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 𝐸 𝑏 ) ≤ ( ( 𝑐 𝐸 𝑎 ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
60 55 56 57 58 59 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 𝐸 𝑏 ) ≤ ( ( 𝑐 𝐸 𝑎 ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
61 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 𝐸 𝑏 ) )
62 12 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
63 13 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
64 14 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
65 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑅 ∈ 𝑍 )
66 62 63 64 65 5 6 55 56 57 imasdsf1o ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) = ( 𝑐 𝐸 𝑎 ) )
67 62 63 64 65 5 6 55 56 58 imasdsf1o ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( 𝑐 𝐸 𝑏 ) )
68 66 67 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) = ( ( 𝑐 𝐸 𝑎 ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
69 60 61 68 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) )
70 69 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ∀ 𝑐 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) )
71 oveq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) )
72 oveq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) )
73 71 72 oveq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) = ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) )
74 73 breq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
75 74 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑧 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ∀ 𝑐 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
76 26 75 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ∀ 𝑐 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
77 32 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
78 76 77 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑐 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ∀ 𝑐 ∈ 𝑉 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( ( 𝐹 ‘ 𝑐 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
80 70 79 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) )
81 54 80 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
82 81 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
83 27 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ) )
84 eqeq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
85 83 84 bibi12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
86 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) )
87 86 oveq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) )
88 27 87 breq12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
89 88 ralbidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) )
90 85 89 anbi12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) ) )
91 90 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) ) )
92 26 91 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) ) )
93 32 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
94 92 93 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
95 94 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 ‘ 𝑏 ) ) ) ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
96 82 95 mpbid ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
97 37 eqeq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ) )
98 eqeq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 = 𝑦 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) )
99 97 98 bibi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ) )
100 oveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) )
101 100 oveq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
102 37 101 breq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
103 102 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
104 99 103 anbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
105 104 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
106 105 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
107 26 106 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
108 32 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
109 107 108 bitr3d ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑦 ∈ 𝐵 ( ( ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 ( 𝐹 ‘ 𝑎 ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
110 96 109 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
111 7 elfvexd ⊢ ( 𝜑 → 𝑉 ∈ V )
112 focdmex ⊢ ( 𝑉 ∈ V → ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐵 ∈ V ) )
113 111 9 112 sylc ⊢ ( 𝜑 → 𝐵 ∈ V )
114 isxmet ⊢ ( 𝐵 ∈ V → ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ↔ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
115 113 114 syl ⊢ ( 𝜑 → ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ↔ ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
116 46 110 115 mpbir2and ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )