Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  istotbnd3 Structured version   Visualization version   GIF version

Theorem istotbnd3 36230
Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
istotbnd3 (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
Distinct variable groups:   𝑣,𝑑,𝑥,𝑀   𝑋,𝑑,𝑣,𝑥

Proof of Theorem istotbnd3
Dummy variables 𝑏 𝑓 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istotbnd 36228 . 2 (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2 oveq1 7364 . . . . . . . . . . . 12 (𝑥 = (𝑓𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓𝑏)(ball‘𝑀)𝑑))
32eqeq2d 2747 . . . . . . . . . . 11 (𝑥 = (𝑓𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))
43ac6sfi 9231 . . . . . . . . . 10 ((𝑤 ∈ Fin ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))
54ex 413 . . . . . . . . 9 (𝑤 ∈ Fin → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))))
65ad2antlr 725 . . . . . . . 8 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))))
7 simprrl 779 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤𝑋)
87frnd 6676 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓𝑋)
9 simplr 767 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
107ffnd 6669 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11 dffn4 6762 . . . . . . . . . . . . . 14 (𝑓 Fn 𝑤𝑓:𝑤onto→ran 𝑓)
1210, 11sylib 217 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤onto→ran 𝑓)
13 fofi 9282 . . . . . . . . . . . . 13 ((𝑤 ∈ Fin ∧ 𝑓:𝑤onto→ran 𝑓) → ran 𝑓 ∈ Fin)
149, 12, 13syl2anc 584 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15 elfpw 9298 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓𝑋 ∧ ran 𝑓 ∈ Fin))
168, 14, 15sylanbrc 583 . . . . . . . . . . 11 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
172eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
1817rexrn 7037 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑤 → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
1910, 18syl 17 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
20 eliun 4958 . . . . . . . . . . . . . 14 (𝑣 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑))
21 eliun 4958 . . . . . . . . . . . . . 14 (𝑣 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑))
2219, 20, 213bitr4g 313 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → (𝑣 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑)))
2322eqrdv 2734 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
24 simprrr 780 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))
25 iuneq2 4973 . . . . . . . . . . . . 13 (∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑) → 𝑏𝑤 𝑏 = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
2624, 25syl 17 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑏𝑤 𝑏 = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
27 uniiun 5018 . . . . . . . . . . . . 13 𝑤 = 𝑏𝑤 𝑏
28 simprl 769 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑤 = 𝑋)
2927, 28eqtr3id 2790 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑏𝑤 𝑏 = 𝑋)
3023, 26, 293eqtr2d 2782 . . . . . . . . . . 11 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31 iuneq1 4970 . . . . . . . . . . . . 13 (𝑣 = ran 𝑓 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
3231eqeq1d 2738 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 → ( 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
3332rspcev 3581 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
3416, 30, 33syl2anc 584 . . . . . . . . . 10 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
3534expr 457 . . . . . . . . 9 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → ((𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3635exlimdv 1936 . . . . . . . 8 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
376, 36syld 47 . . . . . . 7 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3837expimpd 454 . . . . . 6 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) → (( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3938rexlimdva 3152 . . . . 5 (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40 elfpw 9298 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣𝑋𝑣 ∈ Fin))
4140simprbi 497 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
4241ad2antrl 726 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43 mptfi 9295 . . . . . . . . 9 (𝑣 ∈ Fin → (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44 rnfi 9279 . . . . . . . . 9 ((𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
4542, 43, 443syl 18 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46 ovex 7390 . . . . . . . . . 10 (𝑥(ball‘𝑀)𝑑) ∈ V
4746dfiun3 5921 . . . . . . . . 9 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48 simprr 771 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
4947, 48eqtr3id 2790 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50 eqid 2736 . . . . . . . . . 10 (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
5150rnmpt 5910 . . . . . . . . 9 ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
5240simplbi 498 . . . . . . . . . . . 12 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣𝑋)
5352ad2antrl 726 . . . . . . . . . . 11 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣𝑋)
54 ssrexv 4011 . . . . . . . . . . 11 (𝑣𝑋 → (∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
5553, 54syl 17 . . . . . . . . . 10 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
5655ss2abdv 4020 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
5751, 56eqsstrid 3992 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58 unieq 4876 . . . . . . . . . . 11 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → 𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
5958eqeq1d 2738 . . . . . . . . . 10 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ( 𝑤 = 𝑋 ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60 ssabral 4019 . . . . . . . . . . 11 (𝑤 ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61 sseq1 3969 . . . . . . . . . . 11 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
6260, 61bitr3id 284 . . . . . . . . . 10 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
6359, 62anbi12d 631 . . . . . . . . 9 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ( ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
6463rspcev 3581 . . . . . . . 8 ((ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ ( ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
6545, 49, 57, 64syl12anc 835 . . . . . . 7 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
6665expr 457 . . . . . 6 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ( 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
6766rexlimdva 3152 . . . . 5 (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
6839, 67impbid 211 . . . 4 (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
6968ralbidv 3174 . . 3 (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
7069pm5.32i 575 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
711, 70bitri 274 1 (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wral 3064  wrex 3073  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865   ciun 4954  cmpt 5188  ran crn 5634   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  Fincfn 8883  +crp 12915  Metcmet 20782  ballcbl 20783  TotBndctotbnd 36225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-totbnd 36227
This theorem is referenced by:  0totbnd  36232  sstotbnd2  36233  equivtotbnd  36237  totbndbnd  36248  prdstotbnd  36253
  Copyright terms: Public domain W3C validator