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 
|- ( ph -> U = ( F "s R ) )
imasf1oxmet.v 
|- ( ph -> V = ( Base ` R ) )
imasf1oxmet.f 
|- ( ph -> F : V -1-1-onto-> B )
imasf1oxmet.r 
|- ( ph -> R e. Z )
imasf1oxmet.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
imasf1oxmet.d 
|- D = ( dist ` U )
imasf1oxmet.m 
|- ( ph -> E e. ( *Met ` V ) )
Assertion imasf1oxmet 
|- ( ph -> D e. ( *Met ` B ) )

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasf1oxmet.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasf1oxmet.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasf1oxmet.r 
 |-  ( ph -> R e. Z )
5 imasf1oxmet.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
6 imasf1oxmet.d 
 |-  D = ( dist ` U )
7 imasf1oxmet.m 
 |-  ( ph -> E e. ( *Met ` V ) )
8 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
9 3 8 syl 
 |-  ( ph -> F : V -onto-> B )
10 eqid 
 |-  ( dist ` R ) = ( dist ` R )
11 1 2 9 4 10 6 imasdsfn 
 |-  ( ph -> D Fn ( B X. B ) )
12 1 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> U = ( F "s R ) )
13 2 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> V = ( Base ` R ) )
14 3 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> F : V -1-1-onto-> B )
15 4 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> R e. Z )
16 7 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> E e. ( *Met ` V ) )
17 simprl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> a e. V )
18 simprr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> b e. V )
19 12 13 14 15 5 6 16 17 18 imasdsf1o 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) D ( F ` b ) ) = ( a E b ) )
20 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ a e. V /\ b e. V ) -> ( a E b ) e. RR* )
21 20 3expb 
 |-  ( ( E e. ( *Met ` V ) /\ ( a e. V /\ b e. V ) ) -> ( a E b ) e. RR* )
22 7 21 sylan 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a E b ) e. RR* )
23 19 22 eqeltrd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) D ( F ` b ) ) e. RR* )
24 23 ralrimivva 
 |-  ( ph -> A. a e. V A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR* )
25 f1ofn 
 |-  ( F : V -1-1-onto-> B -> F Fn V )
26 3 25 syl 
 |-  ( ph -> F Fn V )
27 oveq2 
 |-  ( y = ( F ` b ) -> ( ( F ` a ) D y ) = ( ( F ` a ) D ( F ` b ) ) )
28 27 eleq1d 
 |-  ( y = ( F ` b ) -> ( ( ( F ` a ) D y ) e. RR* <-> ( ( F ` a ) D ( F ` b ) ) e. RR* ) )
29 28 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR* <-> A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR* ) )
30 26 29 syl 
 |-  ( ph -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR* <-> A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR* ) )
31 forn 
 |-  ( F : V -onto-> B -> ran F = B )
32 9 31 syl 
 |-  ( ph -> ran F = B )
33 32 raleqdv 
 |-  ( ph -> ( A. y e. ran F ( ( F ` a ) D y ) e. RR* <-> A. y e. B ( ( F ` a ) D y ) e. RR* ) )
34 30 33 bitr3d 
 |-  ( ph -> ( A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR* <-> A. y e. B ( ( F ` a ) D y ) e. RR* ) )
35 34 ralbidv 
 |-  ( ph -> ( A. a e. V A. b e. V ( ( F ` a ) D ( F ` b ) ) e. RR* <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR* ) )
36 24 35 mpbid 
 |-  ( ph -> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR* )
37 oveq1 
 |-  ( x = ( F ` a ) -> ( x D y ) = ( ( F ` a ) D y ) )
38 37 eleq1d 
 |-  ( x = ( F ` a ) -> ( ( x D y ) e. RR* <-> ( ( F ` a ) D y ) e. RR* ) )
39 38 ralbidv 
 |-  ( x = ( F ` a ) -> ( A. y e. B ( x D y ) e. RR* <-> A. y e. B ( ( F ` a ) D y ) e. RR* ) )
40 39 ralrn 
 |-  ( F Fn V -> ( A. x e. ran F A. y e. B ( x D y ) e. RR* <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR* ) )
41 26 40 syl 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( x D y ) e. RR* <-> A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR* ) )
42 32 raleqdv 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( x D y ) e. RR* <-> A. x e. B A. y e. B ( x D y ) e. RR* ) )
43 41 42 bitr3d 
 |-  ( ph -> ( A. a e. V A. y e. B ( ( F ` a ) D y ) e. RR* <-> A. x e. B A. y e. B ( x D y ) e. RR* ) )
44 36 43 mpbid 
 |-  ( ph -> A. x e. B A. y e. B ( x D y ) e. RR* )
45 ffnov 
 |-  ( D : ( B X. B ) --> RR* <-> ( D Fn ( B X. B ) /\ A. x e. B A. y e. B ( x D y ) e. RR* ) )
46 11 44 45 sylanbrc 
 |-  ( ph -> D : ( B X. B ) --> RR* )
47 xmeteq0 
 |-  ( ( E e. ( *Met ` V ) /\ a e. V /\ b e. V ) -> ( ( a E b ) = 0 <-> a = b ) )
48 16 17 18 47 syl3anc 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( a E b ) = 0 <-> a = b ) )
49 19 eqeq1d 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( a E b ) = 0 ) )
50 f1of1 
 |-  ( F : V -1-1-onto-> B -> F : V -1-1-> B )
51 3 50 syl 
 |-  ( ph -> F : V -1-1-> B )
52 f1fveq 
 |-  ( ( F : V -1-1-> B /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) = ( F ` b ) <-> a = b ) )
53 51 52 sylan 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( F ` a ) = ( F ` b ) <-> a = b ) )
54 48 49 53 3bitr4d 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) )
55 16 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> E e. ( *Met ` V ) )
56 simpr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> c e. V )
57 17 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> a e. V )
58 18 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> b e. V )
59 xmettri2 
 |-  ( ( E e. ( *Met ` V ) /\ ( c e. V /\ a e. V /\ b e. V ) ) -> ( a E b ) <_ ( ( c E a ) +e ( c E b ) ) )
60 55 56 57 58 59 syl13anc 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( a E b ) <_ ( ( c E a ) +e ( c E b ) ) )
61 19 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( ( F ` a ) D ( F ` b ) ) = ( a E b ) )
62 12 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> U = ( F "s R ) )
63 13 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> V = ( Base ` R ) )
64 14 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> F : V -1-1-onto-> B )
65 15 adantr 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> R e. Z )
66 62 63 64 65 5 6 55 56 57 imasdsf1o 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( ( F ` c ) D ( F ` a ) ) = ( c E a ) )
67 62 63 64 65 5 6 55 56 58 imasdsf1o 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( ( F ` c ) D ( F ` b ) ) = ( c E b ) )
68 66 67 oveq12d 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) = ( ( c E a ) +e ( c E b ) ) )
69 60 61 68 3brtr4d 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) )
70 69 ralrimiva 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. c e. V ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) )
71 oveq1 
 |-  ( z = ( F ` c ) -> ( z D ( F ` a ) ) = ( ( F ` c ) D ( F ` a ) ) )
72 oveq1 
 |-  ( z = ( F ` c ) -> ( z D ( F ` b ) ) = ( ( F ` c ) D ( F ` b ) ) )
73 71 72 oveq12d 
 |-  ( z = ( F ` c ) -> ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) = ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) )
74 73 breq2d 
 |-  ( z = ( F ` c ) -> ( ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) <-> ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) ) )
75 74 ralrn 
 |-  ( F Fn V -> ( A. z e. ran F ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) <-> A. c e. V ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) ) )
76 26 75 syl 
 |-  ( ph -> ( A. z e. ran F ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) <-> A. c e. V ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) ) )
77 32 raleqdv 
 |-  ( ph -> ( A. z e. ran F ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) <-> A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
78 76 77 bitr3d 
 |-  ( ph -> ( A. c e. V ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) <-> A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
79 78 adantr 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( A. c e. V ( ( F ` a ) D ( F ` b ) ) <_ ( ( ( F ` c ) D ( F ` a ) ) +e ( ( F ` c ) D ( F ` b ) ) ) <-> A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
80 70 79 mpbid 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) )
81 54 80 jca 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
82 81 ralrimivva 
 |-  ( ph -> A. a e. V A. b e. V ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
83 27 eqeq1d 
 |-  ( y = ( F ` b ) -> ( ( ( F ` a ) D y ) = 0 <-> ( ( F ` a ) D ( F ` b ) ) = 0 ) )
84 eqeq2 
 |-  ( y = ( F ` b ) -> ( ( F ` a ) = y <-> ( F ` a ) = ( F ` b ) ) )
85 83 84 bibi12d 
 |-  ( y = ( F ` b ) -> ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) <-> ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) ) )
86 oveq2 
 |-  ( y = ( F ` b ) -> ( z D y ) = ( z D ( F ` b ) ) )
87 86 oveq2d 
 |-  ( y = ( F ` b ) -> ( ( z D ( F ` a ) ) +e ( z D y ) ) = ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) )
88 27 87 breq12d 
 |-  ( y = ( F ` b ) -> ( ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) <-> ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
89 88 ralbidv 
 |-  ( y = ( F ` b ) -> ( A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) <-> A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) )
90 85 89 anbi12d 
 |-  ( y = ( F ` b ) -> ( ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) <-> ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) ) )
91 90 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) <-> A. b e. V ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) ) )
92 26 91 syl 
 |-  ( ph -> ( A. y e. ran F ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) <-> A. b e. V ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) ) )
93 32 raleqdv 
 |-  ( ph -> ( A. y e. ran F ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) <-> A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
94 92 93 bitr3d 
 |-  ( ph -> ( A. b e. V ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) <-> A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
95 94 ralbidv 
 |-  ( ph -> ( A. a e. V A. b e. V ( ( ( ( F ` a ) D ( F ` b ) ) = 0 <-> ( F ` a ) = ( F ` b ) ) /\ A. z e. B ( ( F ` a ) D ( F ` b ) ) <_ ( ( z D ( F ` a ) ) +e ( z D ( F ` b ) ) ) ) <-> A. a e. V A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
96 82 95 mpbid 
 |-  ( ph -> A. a e. V A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) )
97 37 eqeq1d 
 |-  ( x = ( F ` a ) -> ( ( x D y ) = 0 <-> ( ( F ` a ) D y ) = 0 ) )
98 eqeq1 
 |-  ( x = ( F ` a ) -> ( x = y <-> ( F ` a ) = y ) )
99 97 98 bibi12d 
 |-  ( x = ( F ` a ) -> ( ( ( x D y ) = 0 <-> x = y ) <-> ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) ) )
100 oveq2 
 |-  ( x = ( F ` a ) -> ( z D x ) = ( z D ( F ` a ) ) )
101 100 oveq1d 
 |-  ( x = ( F ` a ) -> ( ( z D x ) +e ( z D y ) ) = ( ( z D ( F ` a ) ) +e ( z D y ) ) )
102 37 101 breq12d 
 |-  ( x = ( F ` a ) -> ( ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) <-> ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) )
103 102 ralbidv 
 |-  ( x = ( F ` a ) -> ( A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) <-> A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) )
104 99 103 anbi12d 
 |-  ( x = ( F ` a ) -> ( ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) <-> ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
105 104 ralbidv 
 |-  ( x = ( F ` a ) -> ( A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) <-> A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
106 105 ralrn 
 |-  ( F Fn V -> ( A. x e. ran F A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) <-> A. a e. V A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
107 26 106 syl 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) <-> A. a e. V A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) ) )
108 32 raleqdv 
 |-  ( ph -> ( A. x e. ran F A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) <-> A. x e. B A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
109 107 108 bitr3d 
 |-  ( ph -> ( A. a e. V A. y e. B ( ( ( ( F ` a ) D y ) = 0 <-> ( F ` a ) = y ) /\ A. z e. B ( ( F ` a ) D y ) <_ ( ( z D ( F ` a ) ) +e ( z D y ) ) ) <-> A. x e. B A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
110 96 109 mpbid 
 |-  ( ph -> A. x e. B A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
111 7 elfvexd 
 |-  ( ph -> V e. _V )
112 fornex 
 |-  ( V e. _V -> ( F : V -onto-> B -> B e. _V ) )
113 111 9 112 sylc 
 |-  ( ph -> B e. _V )
114 isxmet 
 |-  ( B e. _V -> ( D e. ( *Met ` B ) <-> ( D : ( B X. B ) --> RR* /\ A. x e. B A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
115 113 114 syl 
 |-  ( ph -> ( D e. ( *Met ` B ) <-> ( D : ( B X. B ) --> RR* /\ A. x e. B A. y e. B ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. B ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
116 46 110 115 mpbir2and 
 |-  ( ph -> D e. ( *Met ` B ) )