Metamath Proof Explorer


Theorem sstotbnd2

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 N = M Y × Y
Assertion sstotbnd2 M Met X Y X N TotBnd Y d + v 𝒫 X Fin Y x v x ball M d

Proof

Step Hyp Ref Expression
1 sstotbnd.2 N = M Y × Y
2 metres2 M Met X Y X M Y × Y Met Y
3 1 2 eqeltrid M Met X Y X N Met Y
4 istotbnd3 N TotBnd Y N Met Y d + v 𝒫 Y Fin x v x ball N d = Y
5 4 baib N Met Y N TotBnd Y d + v 𝒫 Y Fin x v x ball N d = Y
6 3 5 syl M Met X Y X N TotBnd Y d + v 𝒫 Y Fin x v x ball N d = Y
7 simpllr M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y Y X
8 7 sspwd M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y 𝒫 Y 𝒫 X
9 8 ssrind M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y 𝒫 Y Fin 𝒫 X Fin
10 simprl M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y v 𝒫 Y Fin
11 9 10 sseldd M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y v 𝒫 X Fin
12 simprr M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y x v x ball N d = Y
13 metxmet M Met X M ∞Met X
14 13 ad4antr M Met X Y X d + v 𝒫 Y Fin x v M ∞Met X
15 elfpw v 𝒫 Y Fin v Y v Fin
16 15 simplbi v 𝒫 Y Fin v Y
17 16 adantl M Met X Y X d + v 𝒫 Y Fin v Y
18 17 sselda M Met X Y X d + v 𝒫 Y Fin x v x Y
19 simp-4r M Met X Y X d + v 𝒫 Y Fin x v Y X
20 sseqin2 Y X X Y = Y
21 19 20 sylib M Met X Y X d + v 𝒫 Y Fin x v X Y = Y
22 18 21 eleqtrrd M Met X Y X d + v 𝒫 Y Fin x v x X Y
23 simpllr M Met X Y X d + v 𝒫 Y Fin x v d +
24 23 rpxrd M Met X Y X d + v 𝒫 Y Fin x v d *
25 1 blres M ∞Met X x X Y d * x ball N d = x ball M d Y
26 14 22 24 25 syl3anc M Met X Y X d + v 𝒫 Y Fin x v x ball N d = x ball M d Y
27 inss1 x ball M d Y x ball M d
28 26 27 eqsstrdi M Met X Y X d + v 𝒫 Y Fin x v x ball N d x ball M d
29 28 ralrimiva M Met X Y X d + v 𝒫 Y Fin x v x ball N d x ball M d
30 ss2iun x v x ball N d x ball M d x v x ball N d x v x ball M d
31 29 30 syl M Met X Y X d + v 𝒫 Y Fin x v x ball N d x v x ball M d
32 31 adantrr M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y x v x ball N d x v x ball M d
33 12 32 eqsstrrd M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y Y x v x ball M d
34 11 33 jca M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y v 𝒫 X Fin Y x v x ball M d
35 34 ex M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y v 𝒫 X Fin Y x v x ball M d
36 35 reximdv2 M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y v 𝒫 X Fin Y x v x ball M d
37 36 ralimdva M Met X Y X d + v 𝒫 Y Fin x v x ball N d = Y d + v 𝒫 X Fin Y x v x ball M d
38 6 37 sylbid M Met X Y X N TotBnd Y d + v 𝒫 X Fin Y x v x ball M d
39 simpr M Met X Y X c + c +
40 39 rphalfcld M Met X Y X c + c 2 +
41 oveq2 d = c 2 x ball M d = x ball M c 2
42 41 iuneq2d d = c 2 x v x ball M d = x v x ball M c 2
43 42 sseq2d d = c 2 Y x v x ball M d Y x v x ball M c 2
44 43 rexbidv d = c 2 v 𝒫 X Fin Y x v x ball M d v 𝒫 X Fin Y x v x ball M c 2
45 44 rspcv c 2 + d + v 𝒫 X Fin Y x v x ball M d v 𝒫 X Fin Y x v x ball M c 2
46 40 45 syl M Met X Y X c + d + v 𝒫 X Fin Y x v x ball M d v 𝒫 X Fin Y x v x ball M c 2
47 elfpw v 𝒫 X Fin v X v Fin
48 47 simprbi v 𝒫 X Fin v Fin
49 48 ad2antrl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 v Fin
50 ssrab2 x v | x ball M c 2 Y v
51 ssfi v Fin x v | x ball M c 2 Y v x v | x ball M c 2 Y Fin
52 49 50 51 sylancl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 x v | x ball M c 2 Y Fin
53 oveq1 x = y x ball M c 2 = y ball M c 2
54 53 ineq1d x = y x ball M c 2 Y = y ball M c 2 Y
55 incom y ball M c 2 Y = Y y ball M c 2
56 54 55 syl6eq x = y x ball M c 2 Y = Y y ball M c 2
57 dfin5 Y y ball M c 2 = z Y | z y ball M c 2
58 56 57 syl6eq x = y x ball M c 2 Y = z Y | z y ball M c 2
59 58 neeq1d x = y x ball M c 2 Y z Y | z y ball M c 2
60 rabn0 z Y | z y ball M c 2 z Y z y ball M c 2
61 59 60 syl6bb x = y x ball M c 2 Y z Y z y ball M c 2
62 61 elrab y x v | x ball M c 2 Y y v z Y z y ball M c 2
63 62 simprbi y x v | x ball M c 2 Y z Y z y ball M c 2
64 63 rgen y x v | x ball M c 2 Y z Y z y ball M c 2
65 eleq1 z = f y z y ball M c 2 f y y ball M c 2
66 65 ac6sfi x v | x ball M c 2 Y Fin y x v | x ball M c 2 Y z Y z y ball M c 2 f f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2
67 52 64 66 sylancl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 f f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2
68 fdm f : x v | x ball M c 2 Y Y dom f = x v | x ball M c 2 Y
69 68 ad2antrl v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 dom f = x v | x ball M c 2 Y
70 69 50 eqsstrdi v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 dom f v
71 simprl v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 f : x v | x ball M c 2 Y Y
72 69 feq2d v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 f : dom f Y f : x v | x ball M c 2 Y Y
73 71 72 mpbird v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 f : dom f Y
74 simprr v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 y x v | x ball M c 2 Y f y y ball M c 2
75 ffn f : x v | x ball M c 2 Y Y f Fn x v | x ball M c 2 Y
76 elpreima f Fn x v | x ball M c 2 Y y f -1 y ball M c 2 y x v | x ball M c 2 Y f y y ball M c 2
77 75 76 syl f : x v | x ball M c 2 Y Y y f -1 y ball M c 2 y x v | x ball M c 2 Y f y y ball M c 2
78 77 baibd f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y y f -1 y ball M c 2 f y y ball M c 2
79 78 ralbidva f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y y f -1 y ball M c 2 y x v | x ball M c 2 Y f y y ball M c 2
80 79 ad2antrl v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 y x v | x ball M c 2 Y y f -1 y ball M c 2 y x v | x ball M c 2 Y f y y ball M c 2
81 74 80 mpbird v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 y x v | x ball M c 2 Y y f -1 y ball M c 2
82 id y = x y = x
83 oveq1 y = x y ball M c 2 = x ball M c 2
84 83 imaeq2d y = x f -1 y ball M c 2 = f -1 x ball M c 2
85 82 84 eleq12d y = x y f -1 y ball M c 2 x f -1 x ball M c 2
86 85 ralrab2 y x v | x ball M c 2 Y y f -1 y ball M c 2 x v x ball M c 2 Y x f -1 x ball M c 2
87 81 86 sylib v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 x v x ball M c 2 Y x f -1 x ball M c 2
88 70 73 87 3jca v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2
89 88 ex v Fin f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2
90 49 89 syl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2
91 simpr2 M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 f : dom f Y
92 91 frnd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 ran f Y
93 91 ffnd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 f Fn dom f
94 49 adantr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 v Fin
95 simpr1 M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 dom f v
96 ssfi v Fin dom f v dom f Fin
97 94 95 96 syl2anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 dom f Fin
98 fnfi f Fn dom f dom f Fin f Fin
99 93 97 98 syl2anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 f Fin
100 rnfi f Fin ran f Fin
101 99 100 syl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 ran f Fin
102 elfpw ran f 𝒫 Y Fin ran f Y ran f Fin
103 92 101 102 sylanbrc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 ran f 𝒫 Y Fin
104 oveq1 x = z x ball N c = z ball N c
105 104 cbviunv x ran f x ball N c = z ran f z ball N c
106 3 ad4antr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f N Met Y
107 metxmet N Met Y N ∞Met Y
108 106 107 syl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f N ∞Met Y
109 92 sselda M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f z Y
110 rpxr c + c *
111 110 ad4antlr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f c *
112 blssm N ∞Met Y z Y c * z ball N c Y
113 108 109 111 112 syl3anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f z ball N c Y
114 113 ralrimiva M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f z ball N c Y
115 iunss z ran f z ball N c Y z ran f z ball N c Y
116 114 115 sylibr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f z ball N c Y
117 iunin1 y v y ball M c 2 Y = y v y ball M c 2 Y
118 simplrr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 Y x v x ball M c 2
119 53 cbviunv x v x ball M c 2 = y v y ball M c 2
120 118 119 sseqtrdi M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 Y y v y ball M c 2
121 sseqin2 Y y v y ball M c 2 y v y ball M c 2 Y = Y
122 120 121 sylib M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y = Y
123 117 122 syl5eq M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y = Y
124 0ss z ran f z ball N c
125 sseq1 y ball M c 2 Y = y ball M c 2 Y z ran f z ball N c z ran f z ball N c
126 124 125 mpbiri y ball M c 2 Y = y ball M c 2 Y z ran f z ball N c
127 126 a1i M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y = y ball M c 2 Y z ran f z ball N c
128 simpr3 M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 x v x ball M c 2 Y x f -1 x ball M c 2
129 54 neeq1d x = y x ball M c 2 Y y ball M c 2 Y
130 id x = y x = y
131 53 imaeq2d x = y f -1 x ball M c 2 = f -1 y ball M c 2
132 130 131 eleq12d x = y x f -1 x ball M c 2 y f -1 y ball M c 2
133 129 132 imbi12d x = y x ball M c 2 Y x f -1 x ball M c 2 y ball M c 2 Y y f -1 y ball M c 2
134 133 rspccva x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y y f -1 y ball M c 2
135 128 134 sylan M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y y f -1 y ball M c 2
136 13 ad5antr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 M ∞Met X
137 cnvimass f -1 y ball M c 2 dom f
138 47 simplbi v 𝒫 X Fin v X
139 138 ad2antrl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 v X
140 139 adantr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 v X
141 95 140 sstrd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 dom f X
142 137 141 sstrid M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 f -1 y ball M c 2 X
143 142 sselda M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 y X
144 simp-4r M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 c +
145 144 rpred M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 c
146 elpreima f Fn dom f y f -1 y ball M c 2 y dom f f y y ball M c 2
147 146 simplbda f Fn dom f y f -1 y ball M c 2 f y y ball M c 2
148 93 147 sylan M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y y ball M c 2
149 blhalf M ∞Met X y X c f y y ball M c 2 y ball M c 2 f y ball M c
150 136 143 145 148 149 syl22anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 y ball M c 2 f y ball M c
151 150 ssrind M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 y ball M c 2 Y f y ball M c Y
152 137 sseli y f -1 y ball M c 2 y dom f
153 ffvelrn f : dom f Y y dom f f y Y
154 91 152 153 syl2an M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y Y
155 simp-5r M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 Y X
156 155 20 sylib M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 X Y = Y
157 154 156 eleqtrrd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y X Y
158 110 ad4antlr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 c *
159 1 blres M ∞Met X f y X Y c * f y ball N c = f y ball M c Y
160 136 157 158 159 syl3anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y ball N c = f y ball M c Y
161 151 160 sseqtrrd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 y ball M c 2 Y f y ball N c
162 fnfvelrn f Fn dom f y dom f f y ran f
163 93 152 162 syl2an M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y ran f
164 oveq1 z = f y z ball N c = f y ball N c
165 164 ssiun2s f y ran f f y ball N c z ran f z ball N c
166 163 165 syl M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 f y ball N c z ran f z ball N c
167 161 166 sstrd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y f -1 y ball M c 2 y ball M c 2 Y z ran f z ball N c
168 167 adantlr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y f -1 y ball M c 2 y ball M c 2 Y z ran f z ball N c
169 168 ex M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y f -1 y ball M c 2 y ball M c 2 Y z ran f z ball N c
170 135 169 syld M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y y ball M c 2 Y z ran f z ball N c
171 127 170 pm2.61dne M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y z ran f z ball N c
172 171 ralrimiva M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y z ran f z ball N c
173 iunss y v y ball M c 2 Y z ran f z ball N c y v y ball M c 2 Y z ran f z ball N c
174 172 173 sylibr M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 y v y ball M c 2 Y z ran f z ball N c
175 123 174 eqsstrrd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 Y z ran f z ball N c
176 116 175 eqssd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 z ran f z ball N c = Y
177 105 176 syl5eq M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 x ran f x ball N c = Y
178 iuneq1 w = ran f x w x ball N c = x ran f x ball N c
179 178 eqeq1d w = ran f x w x ball N c = Y x ran f x ball N c = Y
180 179 rspcev ran f 𝒫 Y Fin x ran f x ball N c = Y w 𝒫 Y Fin x w x ball N c = Y
181 103 177 180 syl2anc M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
182 181 ex M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 dom f v f : dom f Y x v x ball M c 2 Y x f -1 x ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
183 90 182 syld M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
184 183 exlimdv M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 f f : x v | x ball M c 2 Y Y y x v | x ball M c 2 Y f y y ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
185 67 184 mpd M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
186 185 rexlimdvaa M Met X Y X c + v 𝒫 X Fin Y x v x ball M c 2 w 𝒫 Y Fin x w x ball N c = Y
187 46 186 syld M Met X Y X c + d + v 𝒫 X Fin Y x v x ball M d w 𝒫 Y Fin x w x ball N c = Y
188 187 ralrimdva M Met X Y X d + v 𝒫 X Fin Y x v x ball M d c + w 𝒫 Y Fin x w x ball N c = Y
189 istotbnd3 N TotBnd Y N Met Y c + w 𝒫 Y Fin x w x ball N c = Y
190 189 baib N Met Y N TotBnd Y c + w 𝒫 Y Fin x w x ball N c = Y
191 3 190 syl M Met X Y X N TotBnd Y c + w 𝒫 Y Fin x w x ball N c = Y
192 188 191 sylibrd M Met X Y X d + v 𝒫 X Fin Y x v x ball M d N TotBnd Y
193 38 192 impbid M Met X Y X N TotBnd Y d + v 𝒫 X Fin Y x v x ball M d