Theorem istotbnd3 35938

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 35936	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2		oveq1 7291	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
3	2	eqeq2d 2750	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
4	3	ac6sfi 9067	. . . . . . . . . 10 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
5	4	ex 413	. . . . . . . . 9 ⊢ (𝑤 ∈ Fin → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
6	5	ad2antlr 724	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
7		simprrl 778	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤⟶𝑋)
8	7	frnd 6617	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ⊆ 𝑋)
9		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
10	7	ffnd 6610	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11		dffn4 6703	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
12	10, 11	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤–onto→ran 𝑓)
13		fofi 9114	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
14	9, 12, 13	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15		elfpw 9130	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin))
16	8, 14, 15	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
17	2	eleq2d 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
18	17	rexrn 6972	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑤 → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
19	10, 18	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
20		eliun 4929	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑣 ∈ (𝑥(ball‘𝑀)𝑑))
21		eliun 4929	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑤 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑))
22	19, 20, 21	3bitr4g 314	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
23	22	eqrdv 2737	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
24		simprrr 779	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
25		iuneq2 4944	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
27		uniiun 4989	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 = ∪ 𝑏 ∈ 𝑤 𝑏
28		simprl 768	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑤 = 𝑋)
29	27, 28	eqtr3id 2793	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = 𝑋)
30	23, 26, 29	3eqtr2d 2785	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31		iuneq1 4941	. . . . . . . . . . . . 13 ⊢ (𝑣 = ran 𝑓 → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
32	31	eqeq1d 2741	. . . . . . . . . . . 12 ⊢ (𝑣 = ran 𝑓 → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
33	32	rspcev 3562	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
34	16, 30, 33	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
35	34	expr 457	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → ((𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
36	35	exlimdv 1937	. . . . . . . 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 3214	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40		elfpw 9130	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
41	40	simprbi 497	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
42	41	ad2antrl 725	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43		mptfi 9127	. . . . . . . . 9 ⊢ (𝑣 ∈ Fin → (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44		rnfi 9111	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
45	42, 43, 44	3syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46		ovex 7317	. . . . . . . . . 10 ⊢ (𝑥(ball‘𝑀)𝑑) ∈ V
47	46	dfiun3 5878	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48		simprr 770	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
49	47, 48	eqtr3id 2793	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50		eqid 2739	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
51	50	rnmpt 5867	. . . . . . . . 9 ⊢ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
52	40	simplbi 498	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
53	52	ad2antrl 725	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ⊆ 𝑋)
54		ssrexv 3989	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ 𝑋 → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
56	55	ss2abdv 3998	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
57	51, 56	eqsstrid 3970	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58		unieq 4851	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑤 = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
59	58	eqeq1d 2741	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∪ 𝑤 = 𝑋 ↔ ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60		ssabral 3997	. . . . . . . . . . 11 ⊢ (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61		sseq1 3947	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
62	60, 61	bitr3id 285	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
63	59, 62	anbi12d 631	. . . . . . . . 9 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
64	63	rspcev 3562	. . . . . . . 8 ⊢ ((ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
65	45, 49, 57, 64	syl12anc 834	. . . . . . 7 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
66	65	expr 457	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
67	66	rexlimdva 3214	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
68	39, 67	impbid 211	. . . 4 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
69	68	ralbidv 3113	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
70	69	pm5.32i 575	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
71	1, 70	bitri 274	1 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2107  {cab 2716  ∀wral 3065  ∃wrex 3066   ∩ cin 3887   ⊆ wss 3888  𝒫 cpw 4534  ∪ cuni 4840  ∪ ciun 4925   ↦ cmpt 5158  ran crn 5591   Fn wfn 6432  ⟶wf 6433  –onto→wfo 6435  ‘cfv 6437  (class class class)co 7284  Fincfn 8742  ℝ⁺crp 12739  Metcmet 20592  ballcbl 20593  TotBndctotbnd 35933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-1st 7840  df-2nd 7841  df-1o 8306  df-er 8507  df-en 8743  df-dom 8744  df-fin 8746  df-totbnd 35935

This theorem is referenced by:  0totbnd  35940  sstotbnd2  35941  equivtotbnd  35945  totbndbnd  35956  prdstotbnd  35961