Theorem istotbnd3 38138

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.

Step	Hyp	Ref	Expression
1		istotbnd 38136	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2		oveq1 7363	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
3	2	eqeq2d 2750	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
4	3	ac6sfi 9184	. . . . . . . . . 10 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
5	4	ex 413	. . . . . . . . 9 ⊢ (𝑤 ∈ Fin → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
6	5	ad2antlr 733	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
7		simprrl 786	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤⟶𝑋)
8	7	frnd 6663	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ⊆ 𝑋)
9		simplr 774	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
10	7	ffnd 6656	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11		dffn4 6745	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
12	10, 11	sylib 219	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤–onto→ran 𝑓)
13		fofi 9213	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
14	9, 12, 13	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15		elfpw 9254	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin))
16	8, 14, 15	sylanbrc 589	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
17	2	eleq2d 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
18	17	rexrn 7028	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑤 → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
19	10, 18	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
20		eliun 4925	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑))
21		eliun 4925	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑))
22	19, 20, 21	3bitr4g 315	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
23	22	eqrdv 2737	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
24		simprrr 787	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
25		iuneq2 4941	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
27		uniiun 4988	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 = ∪ 𝑏 ∈ 𝑤 𝑏
28		simprl 776	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑤 = 𝑋)
29	27, 28	eqtr3id 2788	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = 𝑋)
30	23, 26, 29	3eqtr2d 2780	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31		iuneq1 4938	. . . . . . . . . . . . 13 ⊢ (𝑣 = ran 𝑓 → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
32	31	eqeq1d 2741	. . . . . . . . . . . 12 ⊢ (𝑣 = ran 𝑓 → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
33	32	rspcev 3560	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
34	16, 30, 33	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
35	34	expr 457	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → ((𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
36	35	exlimdv 1940	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
37	6, 36	syld 47	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
38	37	expimpd 454	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
39	38	rexlimdva 3140	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40		elfpw 9254	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
41	40	simprbi 498	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
42	41	ad2antrl 734	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43		mptfi 9251	. . . . . . . . 9 ⊢ (𝑣 ∈ Fin → (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44		rnfi 9240	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
45	42, 43, 44	3syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46		ovex 7389	. . . . . . . . . 10 ⊢ (𝑥(ball‘𝑀)𝑑) ∈ V
47	46	dfiun3 5912	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48		simprr 778	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
49	47, 48	eqtr3id 2788	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50		eqid 2739	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
51	50	rnmpt 5899	. . . . . . . . 9 ⊢ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
52	40	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
53	52	ad2antrl 734	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ⊆ 𝑋)
54		ssrexv 3984	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ 𝑋 → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
56	55	ss2abdv 3996	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
57	51, 56	eqsstrid 3953	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58		unieq 4849	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑤 = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
59	58	eqeq1d 2741	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∪ 𝑤 = 𝑋 ↔ ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60		ssabral 3995	. . . . . . . . . . 11 ⊢ (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61		sseq1 3940	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
62	60, 61	bitr3id 286	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
63	59, 62	anbi12d 638	. . . . . . . . 9 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
64	63	rspcev 3560	. . . . . . . 8 ⊢ ((ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
65	45, 49, 57, 64	syl12anc 842	. . . . . . 7 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
66	65	expr 457	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
67	66	rexlimdva 3140	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
68	39, 67	impbid 213	. . . 4 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
69	68	ralbidv 3162	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
70	69	pm5.32i 579	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
71	1, 70	bitri 276	1 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  {cab 2717  ∀wral 3053  ∃wrex 3063   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4529  ∪ cuni 4838  ∪ ciun 4921   ↦ cmpt 5153  ran crn 5619   Fn wfn 6480  ⟶wf 6481  –onto→wfo 6483  ‘cfv 6485  (class class class)co 7356  Fincfn 8883  ℝ⁺crp 12933  Metcmet 21333  ballcbl 21334  TotBndctotbnd 38133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-1st 7931  df-2nd 7932  df-1o 8395  df-en 8884  df-dom 8885  df-fin 8887  df-totbnd 38135

This theorem is referenced by:  0totbnd  38140  sstotbnd2  38141  equivtotbnd  38145  totbndbnd  38156  prdstotbnd  38161