Theorem totbndbnd 33588

Description: A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 33568 to only require that 𝑀 be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +∞) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Assertion

Ref	Expression
totbndbnd	⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Bnd‘𝑋))

Proof of Theorem totbndbnd

Dummy variables 𝑣 𝑑 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		totbndmet 33571	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
2		1rp 11836	. . 3 ⊢ 1 ∈ ℝ+
3		istotbnd3 33570	. . . 4 ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
4	3	simprbi 480	. . 3 ⊢ (𝑀 ∈ (TotBnd‘𝑋) → ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)
5		oveq2 6658	. . . . . . 7 ⊢ (𝑑 = 1 → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)1))
6	5	iuneq2d 4547	. . . . . 6 ⊢ (𝑑 = 1 → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1))
7	6	eqeq1d 2624	. . . . 5 ⊢ (𝑑 = 1 → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋))
8	7	rexbidv 3052	. . . 4 ⊢ (𝑑 = 1 → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋))
9	8	rspcv 3305	. . 3 ⊢ (1 ∈ ℝ+ → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋))
10	2, 4, 9	mpsyl 68	. 2 ⊢ (𝑀 ∈ (TotBnd‘𝑋) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)
11		simplll 798	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 𝑀 ∈ (Met‘𝑋))
12		elfpw 8268	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
13	12	simplbi 476	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
14	13	ad2antrl 764	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑣 ⊆ 𝑋)
15	14	sselda 3603	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑋)
16		simpllr 799	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 𝑦 ∈ 𝑋)
17		metcl 22137	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝑀𝑦) ∈ ℝ)
18	11, 15, 16, 17	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → (𝑧𝑀𝑦) ∈ ℝ)
19		metge0 22150	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑧𝑀𝑦))
20	11, 15, 16, 19	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 0 ≤ (𝑧𝑀𝑦))
21	18, 20	ge0p1rpd 11902	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ((𝑧𝑀𝑦) + 1) ∈ ℝ+)
22		eqid 2622	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))
23	21, 22	fmptd 6385	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)):𝑣⟶ℝ+)
24		frn 6053	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)):𝑣⟶ℝ+ → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ+)
25	23, 24	syl 17	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ+)
26	12	simprbi 480	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
27		mptfi 8265	. . . . . . . . . 10 ⊢ (𝑣 ∈ Fin → (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin)
28		rnfi 8249	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin)
29	26, 27, 28	3syl 18	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin)
30	29	ad2antrl 764	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin)
31		simplr 792	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑦 ∈ 𝑋)
32		simprr 796	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)
33	31, 32	eleqtrrd 2704	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑦 ∈ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1))
34		ne0i 3921	. . . . . . . . 9 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ≠ ∅)
35		dm0rn0 5342	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅ ↔ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅)
36		ovex 6678	. . . . . . . . . . . . . . 15 ⊢ ((𝑧𝑀𝑦) + 1) ∈ V
37	36, 22	dmmpti 6023	. . . . . . . . . . . . . 14 ⊢ dom (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = 𝑣
38	37	eqeq1i 2627	. . . . . . . . . . . . 13 ⊢ (dom (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅ ↔ 𝑣 = ∅)
39		iuneq1 4534	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = ∪ 𝑥 ∈ ∅ (𝑥(ball‘𝑀)1))
40	38, 39	sylbi 207	. . . . . . . . . . . 12 ⊢ (dom (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅ → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = ∪ 𝑥 ∈ ∅ (𝑥(ball‘𝑀)1))
41		0iun 4577	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ ∅ (𝑥(ball‘𝑀)1) = ∅
42	40, 41	syl6eq 2672	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅ → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = ∅)
43	35, 42	sylbir 225	. . . . . . . . . 10 ⊢ (ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) = ∅ → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = ∅)
44	43	necon3i 2826	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ≠ ∅ → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅)
45	33, 34, 44	3syl 18	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅)
46		rpssre 11843	. . . . . . . . 9 ⊢ ℝ+ ⊆ ℝ
47	25, 46	syl6ss 3615	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ)
48		ltso 10118	. . . . . . . . 9 ⊢ < Or ℝ
49		fisupcl 8375	. . . . . . . . 9 ⊢ (( < Or ℝ ∧ (ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ)) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
50	48, 49	mpan 706	. . . . . . . 8 ⊢ ((ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
51	30, 45, 47, 50	syl3anc 1326	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
52	25, 51	sseldd 3604	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ+)
53		metxmet 22139	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
54	53	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑀 ∈ (∞Met‘𝑋))
55	54	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋))
56		1red 10055	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → 1 ∈ ℝ)
57	47, 51	sseldd 3604	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ)
58	57	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ)
59	47	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ)
60	45	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅)
61	30	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin)
62		fimaxre2 10969	. . . . . . . . . . . . . . 15 ⊢ ((ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ∈ Fin) → ∃𝑑 ∈ ℝ ∀𝑤 ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))𝑤 ≤ 𝑑)
63	59, 61, 62	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ∃𝑑 ∈ ℝ ∀𝑤 ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))𝑤 ≤ 𝑑)
64	22	elrnmpt1 5374	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑣 ∧ ((𝑧𝑀𝑦) + 1) ∈ V) → ((𝑧𝑀𝑦) + 1) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
65	36, 64	mpan2 707	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑣 → ((𝑧𝑀𝑦) + 1) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
66	65	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ((𝑧𝑀𝑦) + 1) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)))
67		suprub 10984	. . . . . . . . . . . . . 14 ⊢ (((ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ⊆ ℝ ∧ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)) ≠ ∅ ∧ ∃𝑑 ∈ ℝ ∀𝑤 ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))𝑤 ≤ 𝑑) ∧ ((𝑧𝑀𝑦) + 1) ∈ ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))) → ((𝑧𝑀𝑦) + 1) ≤ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))
68	59, 60, 63, 66, 67	syl31anc 1329	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → ((𝑧𝑀𝑦) + 1) ≤ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))
69		leaddsub 10504	. . . . . . . . . . . . . 14 ⊢ (((𝑧𝑀𝑦) ∈ ℝ ∧ 1 ∈ ℝ ∧ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ) → (((𝑧𝑀𝑦) + 1) ≤ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ↔ (𝑧𝑀𝑦) ≤ (sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) − 1)))
70	18, 56, 58, 69	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → (((𝑧𝑀𝑦) + 1) ≤ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ↔ (𝑧𝑀𝑦) ≤ (sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) − 1)))
71	68, 70	mpbid 222	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → (𝑧𝑀𝑦) ≤ (sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) − 1))
72		blss2 22209	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (1 ∈ ℝ ∧ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ ∧ (𝑧𝑀𝑦) ≤ (sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) − 1))) → (𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
73	55, 15, 16, 56, 58, 71, 72	syl33anc 1341	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) ∧ 𝑧 ∈ 𝑣) → (𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
74	73	ralrimiva 2966	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ∀𝑧 ∈ 𝑣 (𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
75		nfcv 2764	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(𝑥(ball‘𝑀)1)
76		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧𝑦
77		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(ball‘𝑀)
78		nfmpt1 4747	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))
79	78	nfrn 5368	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1))
80		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧ℝ
81		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧 <
82	79, 80, 81	nfsup 8357	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )
83	76, 77, 82	nfov 6676	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))
84	75, 83	nfss 3596	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))
85		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))
86		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑀)1) = (𝑧(ball‘𝑀)1))
87	86	sseq1d 3632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )) ↔ (𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))))
88	84, 85, 87	cbvral 3167	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )) ↔ ∀𝑧 ∈ 𝑣 (𝑧(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
89	74, 88	sylibr 224	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
90		iunss 4561	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )) ↔ ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
91	89, 90	sylibr 224	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
92	32, 91	eqsstr3d 3640	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑋 ⊆ (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
93	52	rpxrd 11873	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ*)
94		blssm 22223	. . . . . . . 8 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ*) → (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )) ⊆ 𝑋)
95	54, 31, 93, 94	syl3anc 1326	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )) ⊆ 𝑋)
96	92, 95	eqssd 3620	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → 𝑋 = (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
97		oveq2 6658	. . . . . . . 8 ⊢ (𝑑 = sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) → (𝑦(ball‘𝑀)𝑑) = (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < )))
98	97	eqeq2d 2632	. . . . . . 7 ⊢ (𝑑 = sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) → (𝑋 = (𝑦(ball‘𝑀)𝑑) ↔ 𝑋 = (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))))
99	98	rspcev 3309	. . . . . 6 ⊢ ((sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ) ∈ ℝ+ ∧ 𝑋 = (𝑦(ball‘𝑀)sup(ran (𝑧 ∈ 𝑣 ↦ ((𝑧𝑀𝑦) + 1)), ℝ, < ))) → ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑))
100	52, 96, 99	syl2anc 693	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋)) → ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑))
101	100	rexlimdvaa 3032	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋 → ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑)))
102	101	ralrimdva 2969	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋 → ∀𝑦 ∈ 𝑋 ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑)))
103		isbnd 33579	. . . 4 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑)))
104	103	baib 944	. . 3 ⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (Bnd‘𝑋) ↔ ∀𝑦 ∈ 𝑋 ∃𝑑 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑑)))
105	102, 104	sylibrd 249	. 2 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)1) = 𝑋 → 𝑀 ∈ (Bnd‘𝑋)))
106	1, 10, 105	sylc 65	1 ⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Bnd‘𝑋))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  ∪ ciun 4520   class class class wbr 4653   ↦ cmpt 4729   Or wor 5034  dom cdm 5114  ran crn 5115  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  Fincfn 7955  supcsup 8346  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939  ℝ^*cxr 10073   < clt 10074   ≤ cle 10075   − cmin 10266  ℝ⁺crp 11832  ∞Metcxmt 19731  Metcme 19732  ballcbl 19733  TotBndctotbnd 33565  Bndcbnd 33566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-2 11079  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-totbnd 33567  df-bnd 33578

This theorem is referenced by:  equivbnd2  33591  prdsbnd2  33594  cntotbnd  33595  cnpwstotbnd  33596