Theorem istotbnd3 34497

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 34495	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2		oveq1 6983	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
3	2	eqeq2d 2788	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
4	3	ac6sfi 8557	. . . . . . . . . 10 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
5	4	ex 405	. . . . . . . . 9 ⊢ (𝑤 ∈ Fin → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
6	5	ad2antlr 714	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
7		simprrl 768	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤⟶𝑋)
8	7	frnd 6351	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ⊆ 𝑋)
9		simplr 756	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
10	7	ffnd 6345	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11		dffn4 6425	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
12	10, 11	sylib 210	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤–onto→ran 𝑓)
13		fofi 8605	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
14	9, 12, 13	syl2anc 576	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15		elfpw 8621	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin))
16	8, 14, 15	sylanbrc 575	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
17	2	eleq2d 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
18	17	rexrn 6678	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑤 → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
19	10, 18	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
20		eliun 4796	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑))
21		eliun 4796	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑))
22	19, 20, 21	3bitr4g 306	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
23	22	eqrdv 2776	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
24		simprrr 769	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
25		iuneq2 4810	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
27		uniiun 4848	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 = ∪ 𝑏 ∈ 𝑤 𝑏
28		simprl 758	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑤 = 𝑋)
29	27, 28	syl5eqr 2828	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = 𝑋)
30	23, 26, 29	3eqtr2d 2820	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31		iuneq1 4807	. . . . . . . . . . . . 13 ⊢ (𝑣 = ran 𝑓 → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
32	31	eqeq1d 2780	. . . . . . . . . . . 12 ⊢ (𝑣 = ran 𝑓 → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
33	32	rspcev 3535	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
34	16, 30, 33	syl2anc 576	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
35	34	expr 449	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → ((𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
36	35	exlimdv 1892	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
37	6, 36	syld 47	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
38	37	expimpd 446	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
39	38	rexlimdva 3229	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40		elfpw 8621	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
41	40	simprbi 489	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
42	41	ad2antrl 715	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43		mptfi 8618	. . . . . . . . 9 ⊢ (𝑣 ∈ Fin → (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44		rnfi 8602	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
45	42, 43, 44	3syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46		ovex 7008	. . . . . . . . . 10 ⊢ (𝑥(ball‘𝑀)𝑑) ∈ V
47	46	dfiun3 5679	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48		simprr 760	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
49	47, 48	syl5eqr 2828	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50		eqid 2778	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
51	50	rnmpt 5670	. . . . . . . . 9 ⊢ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
52	40	simplbi 490	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
53	52	ad2antrl 715	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ⊆ 𝑋)
54		ssrexv 3924	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ 𝑋 → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
56	55	ss2abdv 3934	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
57	51, 56	syl5eqss 3905	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58		unieq 4720	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑤 = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
59	58	eqeq1d 2780	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∪ 𝑤 = 𝑋 ↔ ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60		ssabral 3932	. . . . . . . . . . 11 ⊢ (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61		sseq1 3882	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
62	60, 61	syl5bbr 277	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
63	59, 62	anbi12d 621	. . . . . . . . 9 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
64	63	rspcev 3535	. . . . . . . 8 ⊢ ((ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
65	45, 49, 57, 64	syl12anc 824	. . . . . . 7 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
66	65	expr 449	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
67	66	rexlimdva 3229	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
68	39, 67	impbid 204	. . . 4 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
69	68	ralbidv 3147	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
70	69	pm5.32i 567	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
71	1, 70	bitri 267	1 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  ∃wex 1742   ∈ wcel 2050  {cab 2758  ∀wral 3088  ∃wrex 3089   ∩ cin 3828   ⊆ wss 3829  𝒫 cpw 4422  ∪ cuni 4712  ∪ ciun 4792   ↦ cmpt 5008  ran crn 5408   Fn wfn 6183  ⟶wf 6184  –onto→wfo 6186  ‘cfv 6188  (class class class)co 6976  Fincfn 8306  ℝ⁺crp 12204  Metcmet 20233  ballcbl 20234  TotBndctotbnd 34492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-en 8307  df-dom 8308  df-fin 8310  df-totbnd 34494

This theorem is referenced by:  0totbnd  34499  sstotbnd2  34500  equivtotbnd  34504  totbndbnd  34515  prdstotbnd  34520