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=xY,yYFxMFy
Assertion metf1o YAMMetXF:Y1-1 ontoXNMetY

Proof

Step Hyp Ref Expression
1 metf1o.2 N=xY,yYFxMFy
2 f1of F:Y1-1 ontoXF:YX
3 ffvelrn F:YXxYFxX
4 3 ex F:YXxYFxX
5 ffvelrn F:YXyYFyX
6 5 ex F:YXyYFyX
7 4 6 anim12d F:YXxYyYFxXFyX
8 2 7 syl F:Y1-1 ontoXxYyYFxXFyX
9 metcl MMetXFxXFyXFxMFy
10 9 3expib MMetXFxXFyXFxMFy
11 8 10 sylan9r MMetXF:Y1-1 ontoXxYyYFxMFy
12 11 3adant1 YAMMetXF:Y1-1 ontoXxYyYFxMFy
13 12 ralrimivv YAMMetXF:Y1-1 ontoXxYyYFxMFy
14 1 fmpo xYyYFxMFyN:Y×Y
15 13 14 sylib YAMMetXF:Y1-1 ontoXN:Y×Y
16 fveq2 x=uFx=Fu
17 16 oveq1d x=uFxMFy=FuMFy
18 fveq2 y=vFy=Fv
19 18 oveq2d y=vFuMFy=FuMFv
20 ovex FuMFvV
21 17 19 1 20 ovmpo uYvYuNv=FuMFv
22 21 eqeq1d uYvYuNv=0FuMFv=0
23 22 adantl MMetXF:Y1-1 ontoXuYvYuNv=0FuMFv=0
24 ffvelrn F:YXuYFuX
25 24 ex F:YXuYFuX
26 ffvelrn F:YXvYFvX
27 26 ex F:YXvYFvX
28 25 27 anim12d F:YXuYvYFuXFvX
29 2 28 syl F:Y1-1 ontoXuYvYFuXFvX
30 29 imp F:Y1-1 ontoXuYvYFuXFvX
31 30 adantll MMetXF:Y1-1 ontoXuYvYFuXFvX
32 meteq0 MMetXFuXFvXFuMFv=0Fu=Fv
33 32 3expb MMetXFuXFvXFuMFv=0Fu=Fv
34 33 adantlr MMetXF:Y1-1 ontoXFuXFvXFuMFv=0Fu=Fv
35 31 34 syldan MMetXF:Y1-1 ontoXuYvYFuMFv=0Fu=Fv
36 f1of1 F:Y1-1 ontoXF:Y1-1X
37 f1fveq F:Y1-1XuYvYFu=Fvu=v
38 36 37 sylan F:Y1-1 ontoXuYvYFu=Fvu=v
39 38 adantll MMetXF:Y1-1 ontoXuYvYFu=Fvu=v
40 23 35 39 3bitrd MMetXF:Y1-1 ontoXuYvYuNv=0u=v
41 ffvelrn F:YXwYFwX
42 41 ex F:YXwYFwX
43 28 42 anim12d F:YXuYvYwYFuXFvXFwX
44 2 43 syl F:Y1-1 ontoXuYvYwYFuXFvXFwX
45 44 imp F:Y1-1 ontoXuYvYwYFuXFvXFwX
46 45 adantll MMetXF:Y1-1 ontoXuYvYwYFuXFvXFwX
47 mettri2 MMetXFwXFuXFvXFuMFvFwMFu+FwMFv
48 47 expcom FwXFuXFvXMMetXFuMFvFwMFu+FwMFv
49 48 3expb FwXFuXFvXMMetXFuMFvFwMFu+FwMFv
50 49 ancoms FuXFvXFwXMMetXFuMFvFwMFu+FwMFv
51 50 impcom MMetXFuXFvXFwXFuMFvFwMFu+FwMFv
52 51 adantlr MMetXF:Y1-1 ontoXFuXFvXFwXFuMFvFwMFu+FwMFv
53 46 52 syldan MMetXF:Y1-1 ontoXuYvYwYFuMFvFwMFu+FwMFv
54 53 anassrs MMetXF:Y1-1 ontoXuYvYwYFuMFvFwMFu+FwMFv
55 21 adantr uYvYwYuNv=FuMFv
56 fveq2 x=wFx=Fw
57 56 oveq1d x=wFxMFy=FwMFy
58 fveq2 y=uFy=Fu
59 58 oveq2d y=uFwMFy=FwMFu
60 ovex FwMFuV
61 57 59 1 60 ovmpo wYuYwNu=FwMFu
62 61 ancoms uYwYwNu=FwMFu
63 62 adantlr uYvYwYwNu=FwMFu
64 18 oveq2d y=vFwMFy=FwMFv
65 ovex FwMFvV
66 57 64 1 65 ovmpo wYvYwNv=FwMFv
67 66 ancoms vYwYwNv=FwMFv
68 67 adantll uYvYwYwNv=FwMFv
69 63 68 oveq12d uYvYwYwNu+wNv=FwMFu+FwMFv
70 55 69 breq12d uYvYwYuNvwNu+wNvFuMFvFwMFu+FwMFv
71 70 adantll MMetXF:Y1-1 ontoXuYvYwYuNvwNu+wNvFuMFvFwMFu+FwMFv
72 54 71 mpbird MMetXF:Y1-1 ontoXuYvYwYuNvwNu+wNv
73 72 ralrimiva MMetXF:Y1-1 ontoXuYvYwYuNvwNu+wNv
74 40 73 jca MMetXF:Y1-1 ontoXuYvYuNv=0u=vwYuNvwNu+wNv
75 74 3adantl1 YAMMetXF:Y1-1 ontoXuYvYuNv=0u=vwYuNvwNu+wNv
76 75 ex YAMMetXF:Y1-1 ontoXuYvYuNv=0u=vwYuNvwNu+wNv
77 76 ralrimivv YAMMetXF:Y1-1 ontoXuYvYuNv=0u=vwYuNvwNu+wNv
78 ismet YANMetYN:Y×YuYvYuNv=0u=vwYuNvwNu+wNv
79 78 3ad2ant1 YAMMetXF:Y1-1 ontoXNMetYN:Y×YuYvYuNv=0u=vwYuNvwNu+wNv
80 15 77 79 mpbir2and YAMMetXF:Y1-1 ontoXNMetY