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 24925

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 24745	. . . 4 ⊢ 𝐽 ∈ Haus
3		simpl 481	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆ ℂ)
4		cnheibor.3	. . . . 5 ⊢ 𝑇 = (𝐽 ↾_t 𝑋)
5		simpr 483	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp)
6	4, 5	eqeltrrid 2830	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾_t 𝑋) ∈ Comp)
7	1	cnfldtopon 24743	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
8	7	toponunii 22862	. . . . 5 ⊢ ℂ = ∪ 𝐽
9	8	hauscmp 23355	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾_t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
10	2, 3, 6, 9	mp3an2i 1462	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
11	1	cnfldtop 24744	. . . . . . . . . . 11 ⊢ 𝐽 ∈ Top
12	8	restuni 23110	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
13	11, 3, 12	sylancr 585	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
14	4	unieqi 4921	. . . . . . . . . 10 ⊢ ∪ 𝑇 = ∪ (𝐽 ↾_t 𝑋)
15	13, 14	eqtr4di 2783	. . . . . . . . 9 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ 𝑇)
16	15	eleq2d 2811	. . . . . . . 8 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇))
17	16	biimpar 476	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → 𝑥 ∈ 𝑋)
18		cnex 11221	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
19		ssexg 5324	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
20	3, 18, 19	sylancl 584	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V)
21	20	adantr 479	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V)
22		cnxmet 24733	. . . . . . . . . . 11 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
23		0cnd 11239	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ)
24	3	sselda 3976	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ)
25	24	abscld 15419	. . . . . . . . . . . . 13 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
26		peano2re 11419	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
27	25, 26	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ)
28	27	rexrd 11296	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ^*)
29	1	cnfldtopn 24742	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
30	29	blopn 24453	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
31	22, 23, 28, 30	mp3an2i 1462	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
32		elrestr 17413	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
33	11, 21, 31, 32	mp3an2i 1462	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
34	33, 4	eleqtrrdi 2836	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇)
35		0cn 11238	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
36		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24731	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
38	35, 37	mpan 688	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
39		df-neg 11479	. . . . . . . . . . . . . . 15 ⊢ -𝑥 = (0 − 𝑥)
40	39	fveq2i 6899	. . . . . . . . . . . . . 14 ⊢ (abs‘-𝑥) = (abs‘(0 − 𝑥))
41		absneg 15260	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (abs‘-𝑥) = (abs‘𝑥))
42	40, 41	eqtr3id 2779	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(0 − 𝑥)) = (abs‘𝑥))
43	38, 42	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘𝑥))
44	24, 43	syl 17	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
45	25	ltp1d 12177	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1))
46	44, 45	eqbrtrd 5171	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))
47		elbl 24338	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
48	22, 23, 28, 47	mp3an2i 1462	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
49	24, 46, 48	mpbir2and 711	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
50		simpr 483	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
51	49, 50	elind 4192	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
52	24	absge0d 15427	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
53	25, 52	ge0p1rpd 13081	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ⁺)
54		eqid 2725	. . . . . . . . 9 ⊢ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)
55		oveq2 7427	. . . . . . . . . . 11 ⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
56	55	ineq1d 4209	. . . . . . . . . 10 ⊢ (𝑟 = ((abs‘𝑥) + 1) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
57	56	rspceeqv 3628	. . . . . . . . 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 584	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
59		eleq2 2814	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)))
60		eqeq1 2729	. . . . . . . . . . 11 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
61	60	rexbidv 3168	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
62	59, 61	anbi12d 630	. . . . . . . . 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 3606	. . . . . . . 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 835	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
65	17, 64	syldan 589	. . . . . 6 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
66	65	ralrimiva 3135	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
67		eqid 2725	. . . . . 6 ⊢ ∪ 𝑇 = ∪ 𝑇
68		oveq2 7427	. . . . . . . 8 ⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))(𝑓‘𝑢)))
69	68	ineq1d 4209	. . . . . . 7 ⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
70	69	eqeq2d 2736	. . . . . 6 ⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)))
71	67, 70	cmpcovf 23339	. . . . 5 ⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
72	5, 66, 71	syl2anc 582	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
73	15	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇)
74		simpllr 774	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪ 𝑠)
75	73, 74	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠)
76	75	eleq2d 2811	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠))
77		eluni2 4913	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑠 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)
78	76, 77	bitrdi 286	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧))
79		elssuni 4941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠)
80	79	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑠)
81	75	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 = ∪ 𝑠)
82	80, 81	sseqtrrd 4018	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
83		simp-6l 785	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ)
84	82, 83	sstrd 3987	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ)
85		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
86	84, 85	sseldd 3977	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ)
87	86	abscld 15419	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ)
88		simplrl 775	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ)
89		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ⁺)
90	89	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ⁺)
91		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠)
92	90, 91	ffvelcdmd 7094	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ⁺)
93	92	rpred 13051	. . . . . . . . . . . . . 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 6896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
97	96	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ − ))(𝑓‘𝑢)) = (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
98	97	ineq1d 4209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
99	95, 98	eqeq12d 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋)))
100		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
101	100	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
102	99, 101, 91	rspcdva 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
103	85, 102	eleqtrd 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
104	103	elin1d 4196	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
105		0cnd 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ)
106	92	rpxrd 13052	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ^*)
107		elbl 24338	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (𝑓‘𝑧) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
108	22, 105, 106, 107	mp3an2i 1462	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
109	104, 108	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧)))
110	109	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) < (𝑓‘𝑧))
111	94, 110	eqbrtrrd 5173	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧))
112	96	breq1d 5159	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟))
113		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
114	112, 113, 91	rspcdva 3607	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟)
115	87, 93, 88, 111, 114	ltletrd 11406	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟)
116	87, 88, 115	ltled 11394	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟)
117	116	rexlimdvaa 3145	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟))
118	78, 117	sylbid 239	. . . . . . . . . 10 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟))
119	118	ralrimiv 3134	. . . . . . . . 9 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
120		simpllr 774	. . . . . . . . . . 11 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin))
121	120	elin2d 4197	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin)
122		ffvelcdm 7090	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ⁺)
123	122	rpred 13051	. . . . . . . . . . . 12 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ)
124	123	ralrimiva 3135	. . . . . . . . . . 11 ⊢ (𝑓:𝑠⟶ℝ⁺ → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
125	124	ad2antrl 726	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
126		fimaxre3 12193	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
127	121, 125, 126	syl2anc 582	. . . . . . . . 9 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
128	119, 127	reximddv 3160	. . . . . . . 8 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
129	128	ex 411	. . . . . . 7 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → ((𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
130	129	exlimdv 1928	. . . . . 6 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
131	130	expimpd 452	. . . . 5 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
132	131	rexlimdva 3144	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
133	72, 132	mpd 15	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
134	10, 133	jca 510	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
135		eqid 2725	. . . . . 6 ⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧)))
136		eqid 2725	. . . . . 6 ⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟)))
137	1, 4, 135, 136	cnheiborlem 24924	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
138	137	rexlimdvaa 3145	. . . 4 ⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp))
139	138	imp 405	. . 3 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp)
140	139	adantl 480	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
141	134, 140	impbida 799	1 ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 Vcvv 3461 ∩ cin 3943 ⊆ wss 3944 𝒫 cpw 4604 ∪ cuni 4909 class class class wbr 5149 × cxp 5676 “ cima 5681 ∘ ccom 5682 ⟶wf 6545 ‘cfv 6549 (class class class)co 7419 ∈ cmpo 7421 Fincfn 8964 ℂcc 11138 ℝcr 11139 0cc0 11140 1c1 11141 ici 11142 + caddc 11143 · cmul 11145 ℝ^*cxr 11279 < clt 11280 ≤ cle 11281 − cmin 11476 -cneg 11477 ℝ⁺crp 13009 [,]cicc 13362 abscabs 15217 ↾_t crest 17405 TopOpenctopn 17406 ∞Metcxmet 21281 ballcbl 21283 ℂ_fldccnfld 21296 Topctop 22839 Clsdccld 22964 Hauscha 23256 Compccmp 23334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-cnex 11196 ax-resscn 11197 ax-1cn 11198 ax-icn 11199 ax-addcl 11200 ax-addrcl 11201 ax-mulcl 11202 ax-mulrcl 11203 ax-mulcom 11204 ax-addass 11205 ax-mulass 11206 ax-distr 11207 ax-i2m1 11208 ax-1ne0 11209 ax-1rid 11210 ax-rnegex 11211 ax-rrecex 11212 ax-cnre 11213 ax-pre-lttri 11214 ax-pre-lttrn 11215 ax-pre-ltadd 11216 ax-pre-mulgt0 11217 ax-pre-sup 11218 ax-addf 11219

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-iin 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-isom 6558 df-riota 7375 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7685 df-om 7872 df-1st 7994 df-2nd 7995 df-supp 8166 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-er 8725 df-map 8847 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9388 df-fi 9436 df-sup 9467 df-inf 9468 df-oi 9535 df-card 9964 df-pnf 11282 df-mnf 11283 df-xr 11284 df-ltxr 11285 df-le 11286 df-sub 11478 df-neg 11479 df-div 11904 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12506 df-z 12592 df-dec 12711 df-uz 12856 df-q 12966 df-rp 13010 df-xneg 13127 df-xadd 13128 df-xmul 13129 df-ioo 13363 df-icc 13366 df-fz 13520 df-fzo 13663 df-seq 14003 df-exp 14063 df-hash 14326 df-cj 15082 df-re 15083 df-im 15084 df-sqrt 15218 df-abs 15219 df-struct 17119 df-sets 17136 df-slot 17154 df-ndx 17166 df-base 17184 df-ress 17213 df-plusg 17249 df-mulr 17250 df-starv 17251 df-sca 17252 df-vsca 17253 df-ip 17254 df-tset 17255 df-ple 17256 df-ds 17258 df-unif 17259 df-hom 17260 df-cco 17261 df-rest 17407 df-topn 17408 df-0g 17426 df-gsum 17427 df-topgen 17428 df-pt 17429 df-prds 17432 df-xrs 17487 df-qtop 17492 df-imas 17493 df-xps 17495 df-mre 17569 df-mrc 17570 df-acs 17572 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18744 df-mulg 19032 df-cntz 19280 df-cmn 19749 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-cnfld 21297 df-top 22840 df-topon 22857 df-topsp 22879 df-bases 22893 df-cld 22967 df-cls 22969 df-cn 23175 df-cnp 23176 df-haus 23263 df-cmp 23335 df-tx 23510 df-hmeo 23703 df-xms 24270 df-ms 24271 df-tms 24272 df-cncf 24842

This theorem is referenced by: cnllycmp 24926 cncmet 25294 ftalem3 27052

W3C validator