cnheibor - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnheibor		Structured version Visualization version GIF version

Theorem cnheibor 24852

Description: Heine-Borel theorem for complex numbers. A subset of ℂ is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)

**Hypotheses**
Ref	Expression
cnheibor.2	⊢ 𝐽 = (TopOpen‘ℂ_fld)
cnheibor.3	⊢ 𝑇 = (𝐽 ↾_t 𝑋)

**Assertion**
Ref	Expression
cnheibor	⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))

Distinct variable groups: 𝑥,𝑟,𝑇 𝐽,𝑟,𝑥 𝑋,𝑟,𝑥

Proof of Theorem cnheibor Dummy variables 𝑧 𝑢 𝑓 𝑠 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnheibor.2	. . . . 5 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
2	1	cnfldhaus 24670	. . . 4 ⊢ 𝐽 ∈ Haus
3		simpl 482	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆ ℂ)
4		cnheibor.3	. . . . 5 ⊢ 𝑇 = (𝐽 ↾_t 𝑋)
5		simpr 484	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp)
6	4, 5	eqeltrrid 2833	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾_t 𝑋) ∈ Comp)
7	1	cnfldtopon 24668	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
8	7	toponunii 22801	. . . . 5 ⊢ ℂ = ∪ 𝐽
9	8	hauscmp 23292	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾_t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
10	2, 3, 6, 9	mp3an2i 1468	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
11	1	cnfldtop 24669	. . . . . . . . . . 11 ⊢ 𝐽 ∈ Top
12	8	restuni 23047	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
13	11, 3, 12	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
14	4	unieqi 4870	. . . . . . . . . 10 ⊢ ∪ 𝑇 = ∪ (𝐽 ↾_t 𝑋)
15	13, 14	eqtr4di 2782	. . . . . . . . 9 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ 𝑇)
16	15	eleq2d 2814	. . . . . . . 8 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇))
17	16	biimpar 477	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → 𝑥 ∈ 𝑋)
18		cnex 11090	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
19		ssexg 5262	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
20	3, 18, 19	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V)
21	20	adantr 480	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V)
22		cnxmet 24658	. . . . . . . . . . 11 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
23		0cnd 11108	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ)
24	3	sselda 3935	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ)
25	24	abscld 15346	. . . . . . . . . . . . 13 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
26		peano2re 11289	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
27	25, 26	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ)
28	27	rexrd 11165	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ^*)
29	1	cnfldtopn 24667	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
30	29	blopn 24386	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
31	22, 23, 28, 30	mp3an2i 1468	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
32		elrestr 17332	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
33	11, 21, 31, 32	mp3an2i 1468	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
34	33, 4	eleqtrrdi 2839	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇)
35		0cn 11107	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
36		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24656	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
38	35, 37	mpan 690	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
39		df-neg 11350	. . . . . . . . . . . . . . 15 ⊢ -𝑥 = (0 − 𝑥)
40	39	fveq2i 6825	. . . . . . . . . . . . . 14 ⊢ (abs‘-𝑥) = (abs‘(0 − 𝑥))
41		absneg 15184	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (abs‘-𝑥) = (abs‘𝑥))
42	40, 41	eqtr3id 2778	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(0 − 𝑥)) = (abs‘𝑥))
43	38, 42	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘𝑥))
44	24, 43	syl 17	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
45	25	ltp1d 12055	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1))
46	44, 45	eqbrtrd 5114	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))
47		elbl 24274	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
48	22, 23, 28, 47	mp3an2i 1468	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
49	24, 46, 48	mpbir2and 713	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
50		simpr 484	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
51	49, 50	elind 4151	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
52	24	absge0d 15354	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
53	25, 52	ge0p1rpd 12967	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ⁺)
54		eqid 2729	. . . . . . . . 9 ⊢ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)
55		oveq2 7357	. . . . . . . . . . 11 ⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
56	55	ineq1d 4170	. . . . . . . . . 10 ⊢ (𝑟 = ((abs‘𝑥) + 1) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
57	56	rspceeqv 3600	. . . . . . . . 9 ⊢ ((((abs‘𝑥) + 1) ∈ ℝ⁺ ∧ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
58	53, 54, 57	sylancl 586	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
59		eleq2 2817	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)))
60		eqeq1 2733	. . . . . . . . . . 11 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
61	60	rexbidv 3153	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
62	59, 61	anbi12d 632	. . . . . . . . 9 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → ((𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)) ↔ (𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∧ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))))
63	62	rspcev 3577	. . . . . . . 8 ⊢ ((((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇 ∧ (𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∧ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
64	34, 51, 58, 63	syl12anc 836	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
65	17, 64	syldan 591	. . . . . 6 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
66	65	ralrimiva 3121	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
67		eqid 2729	. . . . . 6 ⊢ ∪ 𝑇 = ∪ 𝑇
68		oveq2 7357	. . . . . . . 8 ⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))(𝑓‘𝑢)))
69	68	ineq1d 4170	. . . . . . 7 ⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
70	69	eqeq2d 2740	. . . . . 6 ⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)))
71	67, 70	cmpcovf 23276	. . . . 5 ⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
72	5, 66, 71	syl2anc 584	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
73	15	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇)
74		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪ 𝑠)
75	73, 74	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠)
76	75	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠))
77		eluni2 4862	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑠 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)
78	76, 77	bitrdi 287	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧))
79		elssuni 4888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠)
80	79	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑠)
81	75	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 = ∪ 𝑠)
82	80, 81	sseqtrrd 3973	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
83		simp-6l 786	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ)
84	82, 83	sstrd 3946	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ)
85		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
86	84, 85	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ)
87	86	abscld 15346	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ)
88		simplrl 776	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ)
89		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ⁺)
90	89	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ⁺)
91		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠)
92	90, 91	ffvelcdmd 7019	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ⁺)
93	92	rpred 12937	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ)
94	86, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
95		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
96		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
97	96	oveq2d 7365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ − ))(𝑓‘𝑢)) = (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
98	97	ineq1d 4170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
99	95, 98	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋)))
100		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
101	100	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
102	99, 101, 91	rspcdva 3578	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
103	85, 102	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
104	103	elin1d 4155	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
105		0cnd 11108	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ)
106	92	rpxrd 12938	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ^*)
107		elbl 24274	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (𝑓‘𝑧) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
108	22, 105, 106, 107	mp3an2i 1468	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
109	104, 108	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧)))
110	109	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) < (𝑓‘𝑧))
111	94, 110	eqbrtrrd 5116	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧))
112	96	breq1d 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟))
113		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
114	112, 113, 91	rspcdva 3578	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟)
115	87, 93, 88, 111, 114	ltletrd 11276	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟)
116	87, 88, 115	ltled 11264	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟)
117	116	rexlimdvaa 3131	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟))
118	78, 117	sylbid 240	. . . . . . . . . 10 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟))
119	118	ralrimiv 3120	. . . . . . . . 9 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
120		simpllr 775	. . . . . . . . . . 11 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin))
121	120	elin2d 4156	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin)
122		ffvelcdm 7015	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ⁺)
123	122	rpred 12937	. . . . . . . . . . . 12 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ)
124	123	ralrimiva 3121	. . . . . . . . . . 11 ⊢ (𝑓:𝑠⟶ℝ⁺ → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
125	124	ad2antrl 728	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
126		fimaxre3 12071	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
127	121, 125, 126	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
128	119, 127	reximddv 3145	. . . . . . . 8 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
129	128	ex 412	. . . . . . 7 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → ((𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
130	129	exlimdv 1933	. . . . . 6 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
131	130	expimpd 453	. . . . 5 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
132	131	rexlimdva 3130	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
133	72, 132	mpd 15	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
134	10, 133	jca 511	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
135		eqid 2729	. . . . . 6 ⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧)))
136		eqid 2729	. . . . . 6 ⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟)))
137	1, 4, 135, 136	cnheiborlem 24851	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
138	137	rexlimdvaa 3131	. . . 4 ⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp))
139	138	imp 406	. . 3 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp)
140	139	adantl 481	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
141	134, 140	impbida 800	1 ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3436 ∩ cin 3902 ⊆ wss 3903 𝒫 cpw 4551 ∪ cuni 4858 class class class wbr 5092 × cxp 5617 “ cima 5622 ∘ ccom 5623 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ∈ cmpo 7351 Fincfn 8872 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 ici 11011 + caddc 11012 · cmul 11014 ℝ^*cxr 11148 < clt 11149 ≤ cle 11150 − cmin 11347 -cneg 11348 ℝ⁺crp 12893 [,]cicc 13251 abscabs 15141 ↾_t crest 17324 TopOpenctopn 17325 ∞Metcxmet 21246 ballcbl 21248 ℂ_fldccnfld 21261 Topctop 22778 Clsdccld 22901 Hauscha 23193 Compccmp 23271

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-icc 13255 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-mulg 18947 df-cntz 19196 df-cmn 19661 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-cnfld 21262 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-cls 22906 df-cn 23112 df-cnp 23113 df-haus 23200 df-cmp 23272 df-tx 23447 df-hmeo 23640 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769

This theorem is referenced by: cnllycmp 24853 cncmet 25220 ftalem3 26983

W3C validator