Theorem istotbnd3 35856

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 35854	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
2		oveq1 7262	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
3	2	eqeq2d 2749	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
4	3	ac6sfi 8988	. . . . . . . . . 10 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
5	4	ex 412	. . . . . . . . 9 ⊢ (𝑤 ∈ Fin → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
6	5	ad2antlr 723	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ ∪ 𝑤 = 𝑋) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑓(𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))))
7		simprrl 777	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤⟶𝑋)
8	7	frnd 6592	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ⊆ 𝑋)
9		simplr 765	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑤 ∈ Fin)
10	7	ffnd 6585	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓 Fn 𝑤)
11		dffn4 6678	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
12	10, 11	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → 𝑓:𝑤–onto→ran 𝑓)
13		fofi 9035	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
14	9, 12, 13	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ Fin)
15		elfpw 9051	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin))
16	8, 14, 15	sylanbrc 582	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
17	2	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑣 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
18	17	rexrn 6945	. . . . . . . . . . . . . . 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 313	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → (𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
23	22	eqrdv 2736	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
24		simprrr 778	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
25		iuneq2 4940	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
27		uniiun 4984	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 = ∪ 𝑏 ∈ 𝑤 𝑏
28		simprl 767	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑤 = 𝑋)
29	27, 28	eqtr3id 2793	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑏 ∈ 𝑤 𝑏 = 𝑋)
30	23, 26, 29	3eqtr2d 2784	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋)
31		iuneq1 4937	. . . . . . . . . . . . 13 ⊢ (𝑣 = ran 𝑓 → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
32	31	eqeq1d 2740	. . . . . . . . . . . 12 ⊢ (𝑣 = ran 𝑓 → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋))
33	32	rspcev 3552	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = 𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
34	16, 30, 33	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) ∧ (∪ 𝑤 = 𝑋 ∧ (𝑓:𝑤⟶𝑋 ∧ ∀𝑏 ∈ 𝑤 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
35	34	expr 456	. . . . . . . . 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 453	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑤 ∈ Fin) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
39	38	rexlimdva 3212	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
40		elfpw 9051	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
41	40	simprbi 496	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
42	41	ad2antrl 724	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ∈ Fin)
43		mptfi 9048	. . . . . . . . 9 ⊢ (𝑣 ∈ Fin → (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
44		rnfi 9032	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
45	42, 43, 44	3syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
46		ovex 7288	. . . . . . . . . 10 ⊢ (𝑥(ball‘𝑀)𝑑) ∈ V
47	46	dfiun3 5864	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
48		simprr 769	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
49	47, 48	eqtr3id 2793	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋)
50		eqid 2738	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑))
51	50	rnmpt 5853	. . . . . . . . 9 ⊢ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)}
52	40	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
53	52	ad2antrl 724	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → 𝑣 ⊆ 𝑋)
54		ssrexv 3984	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ 𝑋 → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → (∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
56	55	ss2abdv 3993	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → {𝑏 ∣ ∃𝑥 ∈ 𝑣 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
57	51, 56	eqsstrid 3965	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
58		unieq 4847	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑤 = ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)))
59	58	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∪ 𝑤 = 𝑋 ↔ ∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋))
60		ssabral 3992	. . . . . . . . . . 11 ⊢ (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
61		sseq1 3942	. . . . . . . . . . 11 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑤 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
62	60, 61	bitr3id 284	. . . . . . . . . 10 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
63	59, 62	anbi12d 630	. . . . . . . . 9 ⊢ (𝑤 = ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) → ((∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
64	63	rspcev 3552	. . . . . . . 8 ⊢ ((ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) = 𝑋 ∧ ran (𝑥 ∈ 𝑣 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
65	45, 49, 57, 64	syl12anc 833	. . . . . . 7 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
66	65	expr 456	. . . . . 6 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
67	66	rexlimdva 3212	. . . . 5 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
68	39, 67	impbid 211	. . . 4 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
69	68	ralbidv 3120	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
70	69	pm5.32i 574	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑤 ∈ Fin (∪ 𝑤 = 𝑋 ∧ ∀𝑏 ∈ 𝑤 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
71	1, 70	bitri 274	1 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∃wrex 3064   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530  ∪ cuni 4836  ∪ ciun 4921   ↦ cmpt 5153  ran crn 5581   Fn wfn 6413  ⟶wf 6414  –onto→wfo 6416  ‘cfv 6418  (class class class)co 7255  Fincfn 8691  ℝ⁺crp 12659  Metcmet 20496  ballcbl 20497  TotBndctotbnd 35851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-1st 7804  df-2nd 7805  df-1o 8267  df-er 8456  df-en 8692  df-dom 8693  df-fin 8695  df-totbnd 35853

This theorem is referenced by:  0totbnd  35858  sstotbnd2  35859  equivtotbnd  35863  totbndbnd  35874  prdstotbnd  35879