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 37757
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 37755 . 2 (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2 oveq1 7437 . . . . . . . . . . . 12 (𝑥 = (𝑓𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓𝑏)(ball‘𝑀)𝑑))
32eqeq2d 2745 . . . . . . . . . . 11 (𝑥 = (𝑓𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))
43ac6sfi 9317 . . . . . . . . . 10 ((𝑤 ∈ Fin ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))
54ex 412 . . . . . . . . 9 (𝑤 ∈ Fin → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))))
65ad2antlr 727 . . . . . . . 8 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))))
7 simprrl 781 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤𝑋)
87frnd 6744 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓𝑋)
9 simplr 769 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
107ffnd 6737 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11 dffn4 6826 . . . . . . . . . . . . . 14 (𝑓 Fn 𝑤𝑓:𝑤onto→ran 𝑓)
1210, 11sylib 218 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤onto→ran 𝑓)
13 fofi 9348 . . . . . . . . . . . . 13 ((𝑤 ∈ Fin ∧ 𝑓:𝑤onto→ran 𝑓) → ran 𝑓 ∈ Fin)
149, 12, 13syl2anc 584 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15 elfpw 9391 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓𝑋 ∧ ran 𝑓 ∈ Fin))
168, 14, 15sylanbrc 583 . . . . . . . . . . 11 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
172eleq2d 2824 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
1817rexrn 7106 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑤 → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
1910, 18syl 17 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑)))
20 eliun 4999 . . . . . . . . . . . . . 14 (𝑣 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑))
21 eliun 4999 . . . . . . . . . . . . . 14 (𝑣 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏𝑤 𝑣 ∈ ((𝑓𝑏)(ball‘𝑀)𝑑))
2219, 20, 213bitr4g 314 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → (𝑣 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑)))
2322eqrdv 2732 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
24 simprrr 782 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑))
25 iuneq2 5015 . . . . . . . . . . . . 13 (∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑) → 𝑏𝑤 𝑏 = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
2624, 25syl 17 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑏𝑤 𝑏 = 𝑏𝑤 ((𝑓𝑏)(ball‘𝑀)𝑑))
27 uniiun 5062 . . . . . . . . . . . . 13 𝑤 = 𝑏𝑤 𝑏
28 simprl 771 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑤 = 𝑋)
2927, 28eqtr3id 2788 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑏𝑤 𝑏 = 𝑋)
3023, 26, 293eqtr2d 2780 . . . . . . . . . . 11 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31 iuneq1 5012 . . . . . . . . . . . . 13 (𝑣 = ran 𝑓 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
3231eqeq1d 2736 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 → ( 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
3332rspcev 3621 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
3416, 30, 33syl2anc 584 . . . . . . . . . 10 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ( 𝑤 = 𝑋 ∧ (𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
3534expr 456 . . . . . . . . 9 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → ((𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3635exlimdv 1930 . . . . . . . 8 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∃𝑓(𝑓:𝑤𝑋 ∧ ∀𝑏𝑤 𝑏 = ((𝑓𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
376, 36syld 47 . . . . . . 7 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ 𝑤 = 𝑋) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3837expimpd 453 . . . . . 6 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) → (( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
3938rexlimdva 3152 . . . . 5 (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40 elfpw 9391 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣𝑋𝑣 ∈ Fin))
4140simprbi 496 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
4241ad2antrl 728 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43 mptfi 9388 . . . . . . . . 9 (𝑣 ∈ Fin → (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44 rnfi 9377 . . . . . . . . 9 ((𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
4542, 43, 443syl 18 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46 ovex 7463 . . . . . . . . . 10 (𝑥(ball‘𝑀)𝑑) ∈ V
4746dfiun3 5982 . . . . . . . . 9 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48 simprr 773 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
4947, 48eqtr3id 2788 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50 eqid 2734 . . . . . . . . . 10 (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
5150rnmpt 5970 . . . . . . . . 9 ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
5240simplbi 497 . . . . . . . . . . . 12 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣𝑋)
5352ad2antrl 728 . . . . . . . . . . 11 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣𝑋)
54 ssrexv 4064 . . . . . . . . . . 11 (𝑣𝑋 → (∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
5553, 54syl 17 . . . . . . . . . 10 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
5655ss2abdv 4075 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
5751, 56eqsstrid 4043 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58 unieq 4922 . . . . . . . . . . 11 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → 𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
5958eqeq1d 2736 . . . . . . . . . 10 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ( 𝑤 = 𝑋 ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60 ssabral 4074 . . . . . . . . . . 11 (𝑤 ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61 sseq1 4020 . . . . . . . . . . 11 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
6260, 61bitr3id 285 . . . . . . . . . 10 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
6359, 62anbi12d 632 . . . . . . . . 9 (𝑤 = ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ( ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
6463rspcev 3621 . . . . . . . 8 ((ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ ( ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
6545, 49, 57, 64syl12anc 837 . . . . . . 7 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
6665expr 456 . . . . . 6 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ( 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
6766rexlimdva 3152 . . . . 5 (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
6839, 67impbid 212 . . . 4 (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
6968ralbidv 3175 . . 3 (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
7069pm5.32i 574 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑤 ∈ Fin ( 𝑤 = 𝑋 ∧ ∀𝑏𝑤𝑥𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
711, 70bitri 275 1 (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wex 1775  wcel 2105  {cab 2711  wral 3058  wrex 3067  cin 3961  wss 3962  𝒫 cpw 4604   cuni 4911   ciun 4995  cmpt 5230  ran crn 5689   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  (class class class)co 7430  Fincfn 8983  +crp 13031  Metcmet 21367  ballcbl 21368  TotBndctotbnd 37752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-1st 8012  df-2nd 8013  df-1o 8504  df-en 8984  df-dom 8985  df-fin 8987  df-totbnd 37754
This theorem is referenced by:  0totbnd  37759  sstotbnd2  37760  equivtotbnd  37764  totbndbnd  37775  prdstotbnd  37780
  Copyright terms: Public domain W3C validator