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 fornex ( 𝑉 ∈ 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 ‘ 𝐵 ) )