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 
|- N = ( x e. Y , y e. Y |-> ( ( F ` x ) M ( F ` y ) ) )
Assertion metf1o 
|- ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> N e. ( Met ` Y ) )

Proof

Step Hyp Ref Expression
1 metf1o.2 
 |-  N = ( x e. Y , y e. Y |-> ( ( F ` x ) M ( F ` y ) ) )
2 f1of 
 |-  ( F : Y -1-1-onto-> X -> F : Y --> X )
3 ffvelcdm 
 |-  ( ( F : Y --> X /\ x e. Y ) -> ( F ` x ) e. X )
4 3 ex 
 |-  ( F : Y --> X -> ( x e. Y -> ( F ` x ) e. X ) )
5 ffvelcdm 
 |-  ( ( F : Y --> X /\ y e. Y ) -> ( F ` y ) e. X )
6 5 ex 
 |-  ( F : Y --> X -> ( y e. Y -> ( F ` y ) e. X ) )
7 4 6 anim12d 
 |-  ( F : Y --> X -> ( ( x e. Y /\ y e. Y ) -> ( ( F ` x ) e. X /\ ( F ` y ) e. X ) ) )
8 2 7 syl 
 |-  ( F : Y -1-1-onto-> X -> ( ( x e. Y /\ y e. Y ) -> ( ( F ` x ) e. X /\ ( F ` y ) e. X ) ) )
9 metcl 
 |-  ( ( M e. ( Met ` X ) /\ ( F ` x ) e. X /\ ( F ` y ) e. X ) -> ( ( F ` x ) M ( F ` y ) ) e. RR )
10 9 3expib 
 |-  ( M e. ( Met ` X ) -> ( ( ( F ` x ) e. X /\ ( F ` y ) e. X ) -> ( ( F ` x ) M ( F ` y ) ) e. RR ) )
11 8 10 sylan9r 
 |-  ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> ( ( x e. Y /\ y e. Y ) -> ( ( F ` x ) M ( F ` y ) ) e. RR ) )
12 11 3adant1 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> ( ( x e. Y /\ y e. Y ) -> ( ( F ` x ) M ( F ` y ) ) e. RR ) )
13 12 ralrimivv 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> A. x e. Y A. y e. Y ( ( F ` x ) M ( F ` y ) ) e. RR )
14 1 fmpo 
 |-  ( A. x e. Y A. y e. Y ( ( F ` x ) M ( F ` y ) ) e. RR <-> N : ( Y X. Y ) --> RR )
15 13 14 sylib 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> N : ( Y X. Y ) --> RR )
16 fveq2 
 |-  ( x = u -> ( F ` x ) = ( F ` u ) )
17 16 oveq1d 
 |-  ( x = u -> ( ( F ` x ) M ( F ` y ) ) = ( ( F ` u ) M ( F ` y ) ) )
18 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
19 18 oveq2d 
 |-  ( y = v -> ( ( F ` u ) M ( F ` y ) ) = ( ( F ` u ) M ( F ` v ) ) )
20 ovex 
 |-  ( ( F ` u ) M ( F ` v ) ) e. _V
21 17 19 1 20 ovmpo 
 |-  ( ( u e. Y /\ v e. Y ) -> ( u N v ) = ( ( F ` u ) M ( F ` v ) ) )
22 21 eqeq1d 
 |-  ( ( u e. Y /\ v e. Y ) -> ( ( u N v ) = 0 <-> ( ( F ` u ) M ( F ` v ) ) = 0 ) )
23 22 adantl 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( u N v ) = 0 <-> ( ( F ` u ) M ( F ` v ) ) = 0 ) )
24 ffvelcdm 
 |-  ( ( F : Y --> X /\ u e. Y ) -> ( F ` u ) e. X )
25 24 ex 
 |-  ( F : Y --> X -> ( u e. Y -> ( F ` u ) e. X ) )
26 ffvelcdm 
 |-  ( ( F : Y --> X /\ v e. Y ) -> ( F ` v ) e. X )
27 26 ex 
 |-  ( F : Y --> X -> ( v e. Y -> ( F ` v ) e. X ) )
28 25 27 anim12d 
 |-  ( F : Y --> X -> ( ( u e. Y /\ v e. Y ) -> ( ( F ` u ) e. X /\ ( F ` v ) e. X ) ) )
29 2 28 syl 
 |-  ( F : Y -1-1-onto-> X -> ( ( u e. Y /\ v e. Y ) -> ( ( F ` u ) e. X /\ ( F ` v ) e. X ) ) )
30 29 imp 
 |-  ( ( F : Y -1-1-onto-> X /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` u ) e. X /\ ( F ` v ) e. X ) )
31 30 adantll 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` u ) e. X /\ ( F ` v ) e. X ) )
32 meteq0 
 |-  ( ( M e. ( Met ` X ) /\ ( F ` u ) e. X /\ ( F ` v ) e. X ) -> ( ( ( F ` u ) M ( F ` v ) ) = 0 <-> ( F ` u ) = ( F ` v ) ) )
33 32 3expb 
 |-  ( ( M e. ( Met ` X ) /\ ( ( F ` u ) e. X /\ ( F ` v ) e. X ) ) -> ( ( ( F ` u ) M ( F ` v ) ) = 0 <-> ( F ` u ) = ( F ` v ) ) )
34 33 adantlr 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( ( F ` u ) e. X /\ ( F ` v ) e. X ) ) -> ( ( ( F ` u ) M ( F ` v ) ) = 0 <-> ( F ` u ) = ( F ` v ) ) )
35 31 34 syldan 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( ( F ` u ) M ( F ` v ) ) = 0 <-> ( F ` u ) = ( F ` v ) ) )
36 f1of1 
 |-  ( F : Y -1-1-onto-> X -> F : Y -1-1-> X )
37 f1fveq 
 |-  ( ( F : Y -1-1-> X /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` u ) = ( F ` v ) <-> u = v ) )
38 36 37 sylan 
 |-  ( ( F : Y -1-1-onto-> X /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` u ) = ( F ` v ) <-> u = v ) )
39 38 adantll 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( F ` u ) = ( F ` v ) <-> u = v ) )
40 23 35 39 3bitrd 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( u N v ) = 0 <-> u = v ) )
41 ffvelcdm 
 |-  ( ( F : Y --> X /\ w e. Y ) -> ( F ` w ) e. X )
42 41 ex 
 |-  ( F : Y --> X -> ( w e. Y -> ( F ` w ) e. X ) )
43 28 42 anim12d 
 |-  ( F : Y --> X -> ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) ) )
44 2 43 syl 
 |-  ( F : Y -1-1-onto-> X -> ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) ) )
45 44 imp 
 |-  ( ( F : Y -1-1-onto-> X /\ ( ( u e. Y /\ v e. Y ) /\ w e. Y ) ) -> ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) )
46 45 adantll 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( ( u e. Y /\ v e. Y ) /\ w e. Y ) ) -> ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) )
47 mettri2 
 |-  ( ( M e. ( Met ` X ) /\ ( ( F ` w ) e. X /\ ( F ` u ) e. X /\ ( F ` v ) e. X ) ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
48 47 expcom 
 |-  ( ( ( F ` w ) e. X /\ ( F ` u ) e. X /\ ( F ` v ) e. X ) -> ( M e. ( Met ` X ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) ) )
49 48 3expb 
 |-  ( ( ( F ` w ) e. X /\ ( ( F ` u ) e. X /\ ( F ` v ) e. X ) ) -> ( M e. ( Met ` X ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) ) )
50 49 ancoms 
 |-  ( ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) -> ( M e. ( Met ` X ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) ) )
51 50 impcom 
 |-  ( ( M e. ( Met ` X ) /\ ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
52 51 adantlr 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( ( ( F ` u ) e. X /\ ( F ` v ) e. X ) /\ ( F ` w ) e. X ) ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
53 46 52 syldan 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( ( u e. Y /\ v e. Y ) /\ w e. Y ) ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
54 53 anassrs 
 |-  ( ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) /\ w e. Y ) -> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
55 21 adantr 
 |-  ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( u N v ) = ( ( F ` u ) M ( F ` v ) ) )
56 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
57 56 oveq1d 
 |-  ( x = w -> ( ( F ` x ) M ( F ` y ) ) = ( ( F ` w ) M ( F ` y ) ) )
58 fveq2 
 |-  ( y = u -> ( F ` y ) = ( F ` u ) )
59 58 oveq2d 
 |-  ( y = u -> ( ( F ` w ) M ( F ` y ) ) = ( ( F ` w ) M ( F ` u ) ) )
60 ovex 
 |-  ( ( F ` w ) M ( F ` u ) ) e. _V
61 57 59 1 60 ovmpo 
 |-  ( ( w e. Y /\ u e. Y ) -> ( w N u ) = ( ( F ` w ) M ( F ` u ) ) )
62 61 ancoms 
 |-  ( ( u e. Y /\ w e. Y ) -> ( w N u ) = ( ( F ` w ) M ( F ` u ) ) )
63 62 adantlr 
 |-  ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( w N u ) = ( ( F ` w ) M ( F ` u ) ) )
64 18 oveq2d 
 |-  ( y = v -> ( ( F ` w ) M ( F ` y ) ) = ( ( F ` w ) M ( F ` v ) ) )
65 ovex 
 |-  ( ( F ` w ) M ( F ` v ) ) e. _V
66 57 64 1 65 ovmpo 
 |-  ( ( w e. Y /\ v e. Y ) -> ( w N v ) = ( ( F ` w ) M ( F ` v ) ) )
67 66 ancoms 
 |-  ( ( v e. Y /\ w e. Y ) -> ( w N v ) = ( ( F ` w ) M ( F ` v ) ) )
68 67 adantll 
 |-  ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( w N v ) = ( ( F ` w ) M ( F ` v ) ) )
69 63 68 oveq12d 
 |-  ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( ( w N u ) + ( w N v ) ) = ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) )
70 55 69 breq12d 
 |-  ( ( ( u e. Y /\ v e. Y ) /\ w e. Y ) -> ( ( u N v ) <_ ( ( w N u ) + ( w N v ) ) <-> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) ) )
71 70 adantll 
 |-  ( ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) /\ w e. Y ) -> ( ( u N v ) <_ ( ( w N u ) + ( w N v ) ) <-> ( ( F ` u ) M ( F ` v ) ) <_ ( ( ( F ` w ) M ( F ` u ) ) + ( ( F ` w ) M ( F ` v ) ) ) ) )
72 54 71 mpbird 
 |-  ( ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) /\ w e. Y ) -> ( u N v ) <_ ( ( w N u ) + ( w N v ) ) )
73 72 ralrimiva 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) )
74 40 73 jca 
 |-  ( ( ( M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) )
75 74 3adantl1 
 |-  ( ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) /\ ( u e. Y /\ v e. Y ) ) -> ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) )
76 75 ex 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> ( ( u e. Y /\ v e. Y ) -> ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) ) )
77 76 ralrimivv 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> A. u e. Y A. v e. Y ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) )
78 ismet 
 |-  ( Y e. A -> ( N e. ( Met ` Y ) <-> ( N : ( Y X. Y ) --> RR /\ A. u e. Y A. v e. Y ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) ) ) )
79 78 3ad2ant1 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> ( N e. ( Met ` Y ) <-> ( N : ( Y X. Y ) --> RR /\ A. u e. Y A. v e. Y ( ( ( u N v ) = 0 <-> u = v ) /\ A. w e. Y ( u N v ) <_ ( ( w N u ) + ( w N v ) ) ) ) ) )
80 15 77 79 mpbir2and 
 |-  ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> N e. ( Met ` Y ) )