Theorem sstotbnd 36643

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Hypothesis

Ref	Expression
sstotbnd.2	⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))

Assertion

Ref	Expression
sstotbnd	⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))

Distinct variable groups:   𝑏,𝑑,𝑣,𝑥,𝑀   𝑋,𝑏,𝑑,𝑣,𝑥   𝑁,𝑑,𝑣,𝑥   𝑌,𝑏,𝑑,𝑣,𝑥

Allowed substitution hint:   𝑁(𝑏)

Proof of Theorem sstotbnd

Dummy variables 𝑓 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sstotbnd.2	. . 3 ⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))
2	1	sstotbnd2 36642	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑)))
3		elfpw 9354	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑢 ⊆ 𝑋 ∧ 𝑢 ∈ Fin))
4	3	simprbi 498	. . . . . . . 8 ⊢ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) → 𝑢 ∈ Fin)
5		mptfi 9351	. . . . . . . 8 ⊢ (𝑢 ∈ Fin → (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
6		rnfi 9335	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin → ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
7	4, 5, 6	3syl 18	. . . . . . 7 ⊢ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) → ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
8	7	ad2antrl 727	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin)
9		simprr 772	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))
10		eqid 2733	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) = (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑))
11	10	rnmpt 5955	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) = {𝑏 ∣ ∃𝑥 ∈ 𝑢 𝑏 = (𝑥(ball‘𝑀)𝑑)}
12	3	simplbi 499	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) → 𝑢 ⊆ 𝑋)
13		ssrexv 4052	. . . . . . . . . 10 ⊢ (𝑢 ⊆ 𝑋 → (∃𝑥 ∈ 𝑢 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) → (∃𝑥 ∈ 𝑢 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
15	14	ad2antrl 727	. . . . . . . 8 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → (∃𝑥 ∈ 𝑢 𝑏 = (𝑥(ball‘𝑀)𝑑) → ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
16	15	ss2abdv 4061	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → {𝑏 ∣ ∃𝑥 ∈ 𝑢 𝑏 = (𝑥(ball‘𝑀)𝑑)} ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
17	11, 16	eqsstrid 4031	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})
18		unieq 4920	. . . . . . . . . 10 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑣 = ∪ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)))
19		ovex 7442	. . . . . . . . . . 11 ⊢ (𝑥(ball‘𝑀)𝑑) ∈ V
20	19	dfiun3 5966	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) = ∪ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑))
21	18, 20	eqtr4di 2791	. . . . . . . . 9 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → ∪ 𝑣 = ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))
22	21	sseq2d 4015	. . . . . . . 8 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑌 ⊆ ∪ 𝑣 ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑)))
23		ssabral 4060	. . . . . . . . 9 ⊢ (𝑣 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))
24		sseq1 4008	. . . . . . . . 9 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → (𝑣 ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)} ↔ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
25	23, 24	bitr3id 285	. . . . . . . 8 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → (∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)}))
26	22, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑣 = ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) → ((𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) ↔ (𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) ∧ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})))
27	26	rspcev 3613	. . . . . 6 ⊢ ((ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) ∧ ran (𝑥 ∈ 𝑢 ↦ (𝑥(ball‘𝑀)𝑑)) ⊆ {𝑏 ∣ ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)})) → ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
28	8, 9, 17, 27	syl12anc 836	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑢 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))) → ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))
29	28	rexlimdvaa 3157	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
30		oveq1 7416	. . . . . . . . . 10 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑥(ball‘𝑀)𝑑) = ((𝑓‘𝑏)(ball‘𝑀)𝑑))
31	30	eqeq2d 2744	. . . . . . . . 9 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑏 = (𝑥(ball‘𝑀)𝑑) ↔ 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
32	31	ac6sfi 9287	. . . . . . . 8 ⊢ ((𝑣 ∈ Fin ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑓(𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
33	32	adantrl 715	. . . . . . 7 ⊢ ((𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))) → ∃𝑓(𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
34	33	adantl 483	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) → ∃𝑓(𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
35		frn 6725	. . . . . . . . 9 ⊢ (𝑓:𝑣⟶𝑋 → ran 𝑓 ⊆ 𝑋)
36	35	ad2antrl 727	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ran 𝑓 ⊆ 𝑋)
37		simplrl 776	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑣 ∈ Fin)
38		ffn 6718	. . . . . . . . . . 11 ⊢ (𝑓:𝑣⟶𝑋 → 𝑓 Fn 𝑣)
39	38	ad2antrl 727	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑓 Fn 𝑣)
40		dffn4 6812	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑣 ↔ 𝑓:𝑣–onto→ran 𝑓)
41	39, 40	sylib 217	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑓:𝑣–onto→ran 𝑓)
42		fofi 9338	. . . . . . . . 9 ⊢ ((𝑣 ∈ Fin ∧ 𝑓:𝑣–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
43	37, 41, 42	syl2anc 585	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ran 𝑓 ∈ Fin)
44		elfpw 9354	. . . . . . . 8 ⊢ (ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin))
45	36, 43, 44	sylanbrc 584	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin))
46		simprrl 780	. . . . . . . . . 10 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) → 𝑌 ⊆ ∪ 𝑣)
47	46	adantr 482	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑌 ⊆ ∪ 𝑣)
48		uniiun 5062	. . . . . . . . . . 11 ⊢ ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 𝑏
49		iuneq2 5017	. . . . . . . . . . 11 ⊢ (∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑏 ∈ 𝑣 𝑏 = ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
50	48, 49	eqtrid 2785	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑) → ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
51	50	ad2antll 728	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
52	47, 51	sseqtrd 4023	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑌 ⊆ ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
53	30	eleq2d 2820	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑏) → (𝑦 ∈ (𝑥(ball‘𝑀)𝑑) ↔ 𝑦 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
54	53	rexrn 7089	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑣 → (∃𝑥 ∈ ran 𝑓 𝑦 ∈ (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑣 𝑦 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
55		eliun 5002	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ ∃𝑥 ∈ ran 𝑓 𝑦 ∈ (𝑥(ball‘𝑀)𝑑))
56		eliun 5002	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑) ↔ ∃𝑏 ∈ 𝑣 𝑦 ∈ ((𝑓‘𝑏)(ball‘𝑀)𝑑))
57	54, 55, 56	3bitr4g 314	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑣 → (𝑦 ∈ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) ↔ 𝑦 ∈ ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑)))
58	57	eqrdv 2731	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑣 → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
59	39, 58	syl 17	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑) = ∪ 𝑏 ∈ 𝑣 ((𝑓‘𝑏)(ball‘𝑀)𝑑))
60	52, 59	sseqtrrd 4024	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
61		iuneq1 5014	. . . . . . . . 9 ⊢ (𝑢 = ran 𝑓 → ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑))
62	61	sseq2d 4015	. . . . . . . 8 ⊢ (𝑢 = ran 𝑓 → (𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑)))
63	62	rspcev 3613	. . . . . . 7 ⊢ ((ran 𝑓 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑀)𝑑)) → ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))
64	45, 60, 63	syl2anc 585	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) ∧ (𝑓:𝑣⟶𝑋 ∧ ∀𝑏 ∈ 𝑣 𝑏 = ((𝑓‘𝑏)(ball‘𝑀)𝑑))) → ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))
65	34, 64	exlimddv 1939	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑣 ∈ Fin ∧ (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) → ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑))
66	65	rexlimdvaa 3157	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)) → ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑)))
67	29, 66	impbid 211	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
68	67	ralbidv 3178	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑢 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 (𝑥(ball‘𝑀)𝑑) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
69	2, 68	bitrd 279	1 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  ∀wral 3062  ∃wrex 3071   ∩ cin 3948   ⊆ wss 3949  𝒫 cpw 4603  ∪ cuni 4909  ∪ ciun 4998   ↦ cmpt 5232   × cxp 5675  ran crn 5678   ↾ cres 5679   Fn wfn 6539  ⟶wf 6540  –onto→wfo 6542  ‘cfv 6544  (class class class)co 7409  Fincfn 8939  ℝ⁺crp 12974  Metcmet 20930  ballcbl 20931  TotBndctotbnd 36634

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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-2 12275  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-totbnd 36636

This theorem is referenced by:  totbndss  36645