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 24927

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 482	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆ ℂ)
4		cnheibor.3	. . . . 5 ⊢ 𝑇 = (𝐽 ↾_t 𝑋)
5		simpr 484	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp)
6	4, 5	eqeltrrid 2842	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾_t 𝑋) ∈ Comp)
7	1	cnfldtopon 24743	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
8	7	toponunii 22877	. . . . 5 ⊢ ℂ = ∪ 𝐽
9	8	hauscmp 23368	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾_t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
10	2, 3, 6, 9	mp3an2i 1469	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
11	1	cnfldtop 24744	. . . . . . . . . . 11 ⊢ 𝐽 ∈ Top
12	8	restuni 23123	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
13	11, 3, 12	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
14	4	unieqi 4877	. . . . . . . . . 10 ⊢ ∪ 𝑇 = ∪ (𝐽 ↾_t 𝑋)
15	13, 14	eqtr4di 2790	. . . . . . . . 9 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ 𝑇)
16	15	eleq2d 2823	. . . . . . . 8 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇))
17	16	biimpar 477	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → 𝑥 ∈ 𝑋)
18		cnex 11121	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
19		ssexg 5272	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
20	3, 18, 19	sylancl 587	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V)
21	20	adantr 480	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V)
22		cnxmet 24733	. . . . . . . . . . 11 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
23		0cnd 11139	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ)
24	3	sselda 3935	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ)
25	24	abscld 15376	. . . . . . . . . . . . 13 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
26		peano2re 11320	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
27	25, 26	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ)
28	27	rexrd 11196	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ^*)
29	1	cnfldtopn 24742	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
30	29	blopn 24461	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
31	22, 23, 28, 30	mp3an2i 1469	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
32		elrestr 17362	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
33	11, 21, 31, 32	mp3an2i 1469	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
34	33, 4	eleqtrrdi 2848	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇)
35		0cn 11138	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
36		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24731	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
38	35, 37	mpan 691	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
39		df-neg 11381	. . . . . . . . . . . . . . 15 ⊢ -𝑥 = (0 − 𝑥)
40	39	fveq2i 6847	. . . . . . . . . . . . . 14 ⊢ (abs‘-𝑥) = (abs‘(0 − 𝑥))
41		absneg 15214	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (abs‘-𝑥) = (abs‘𝑥))
42	40, 41	eqtr3id 2786	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(0 − 𝑥)) = (abs‘𝑥))
43	38, 42	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘𝑥))
44	24, 43	syl 17	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
45	25	ltp1d 12086	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1))
46	44, 45	eqbrtrd 5122	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))
47		elbl 24349	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
48	22, 23, 28, 47	mp3an2i 1469	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
49	24, 46, 48	mpbir2and 714	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
50		simpr 484	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
51	49, 50	elind 4154	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
52	24	absge0d 15384	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
53	25, 52	ge0p1rpd 12993	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ⁺)
54		eqid 2737	. . . . . . . . 9 ⊢ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)
55		oveq2 7378	. . . . . . . . . . 11 ⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
56	55	ineq1d 4173	. . . . . . . . . 10 ⊢ (𝑟 = ((abs‘𝑥) + 1) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
57	56	rspceeqv 3601	. . . . . . . . 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 587	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
59		eleq2 2826	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)))
60		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
61	60	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
62	59, 61	anbi12d 633	. . . . . . . . 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 3578	. . . . . . . 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 837	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
65	17, 64	syldan 592	. . . . . 6 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
66	65	ralrimiva 3130	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
67		eqid 2737	. . . . . 6 ⊢ ∪ 𝑇 = ∪ 𝑇
68		oveq2 7378	. . . . . . . 8 ⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))(𝑓‘𝑢)))
69	68	ineq1d 4173	. . . . . . 7 ⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
70	69	eqeq2d 2748	. . . . . 6 ⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)))
71	67, 70	cmpcovf 23352	. . . . 5 ⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
72	5, 66, 71	syl2anc 585	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
73	15	ad4antr 733	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇)
74		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪ 𝑠)
75	73, 74	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠)
76	75	eleq2d 2823	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠))
77		eluni2 4869	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑠 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)
78	76, 77	bitrdi 287	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧))
79		elssuni 4896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠)
80	79	ad2antrl 729	. . . . . . . . . . . . . . . . 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 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ)
84	82, 83	sstrd 3946	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ)
85		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
86	84, 85	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ)
87	86	abscld 15376	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ)
88		simplrl 777	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ)
89		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ⁺)
90	89	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ⁺)
91		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠)
92	90, 91	ffvelcdmd 7041	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ⁺)
93	92	rpred 12963	. . . . . . . . . . . . . 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 6844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
97	96	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ − ))(𝑓‘𝑢)) = (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
98	97	ineq1d 4173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
99	95, 98	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋)))
100		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
101	100	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
102	99, 101, 91	rspcdva 3579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
103	85, 102	eleqtrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
104	103	elin1d 4158	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
105		0cnd 11139	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ)
106	92	rpxrd 12964	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ^*)
107		elbl 24349	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (𝑓‘𝑧) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
108	22, 105, 106, 107	mp3an2i 1469	. . . . . . . . . . . . . . . . 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 5124	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧))
112	96	breq1d 5110	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟))
113		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
114	112, 113, 91	rspcdva 3579	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟)
115	87, 93, 88, 111, 114	ltletrd 11307	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟)
116	87, 88, 115	ltled 11295	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟)
117	116	rexlimdvaa 3140	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟))
118	78, 117	sylbid 240	. . . . . . . . . 10 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟))
119	118	ralrimiv 3129	. . . . . . . . 9 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
120		simpllr 776	. . . . . . . . . . 11 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin))
121	120	elin2d 4159	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin)
122		ffvelcdm 7037	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ⁺)
123	122	rpred 12963	. . . . . . . . . . . 12 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ)
124	123	ralrimiva 3130	. . . . . . . . . . 11 ⊢ (𝑓:𝑠⟶ℝ⁺ → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
125	124	ad2antrl 729	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
126		fimaxre3 12102	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
127	121, 125, 126	syl2anc 585	. . . . . . . . 9 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
128	119, 127	reximddv 3154	. . . . . . . 8 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
129	128	ex 412	. . . . . . 7 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → ((𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
130	129	exlimdv 1935	. . . . . 6 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
131	130	expimpd 453	. . . . 5 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
132	131	rexlimdva 3139	. . . 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 2737	. . . . . 6 ⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧)))
136		eqid 2737	. . . . . 6 ⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟)))
137	1, 4, 135, 136	cnheiborlem 24926	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
138	137	rexlimdvaa 3140	. . . 4 ⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp))
139	138	imp 406	. . 3 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp)
140	139	adantl 481	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
141	134, 140	impbida 801	1 ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ∩ cin 3902 ⊆ wss 3903 𝒫 cpw 4556 ∪ cuni 4865 class class class wbr 5100 × cxp 5632 “ cima 5637 ∘ ccom 5638 ⟶wf 6498 ‘cfv 6502 (class class class)co 7370 ∈ cmpo 7372 Fincfn 8897 ℂcc 11038 ℝcr 11039 0cc0 11040 1c1 11041 ici 11042 + caddc 11043 · cmul 11045 ℝ^*cxr 11179 < clt 11180 ≤ cle 11181 − cmin 11378 -cneg 11379 ℝ⁺crp 12919 [,]cicc 13278 abscabs 15171 ↾_t crest 17354 TopOpenctopn 17355 ∞Metcxmet 21311 ballcbl 21313 ℂ_fldccnfld 21326 Topctop 22854 Clsdccld 22977 Hauscha 23269 Compccmp 23347

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118 ax-addf 11119

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-se 5588 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-isom 6511 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-of 7634 df-om 7821 df-1st 7945 df-2nd 7946 df-supp 8115 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-2o 8410 df-er 8647 df-map 8779 df-ixp 8850 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-fsupp 9279 df-fi 9328 df-sup 9359 df-inf 9360 df-oi 9429 df-card 9865 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-5 12225 df-6 12226 df-7 12227 df-8 12228 df-9 12229 df-n0 12416 df-z 12503 df-dec 12622 df-uz 12766 df-q 12876 df-rp 12920 df-xneg 13040 df-xadd 13041 df-xmul 13042 df-ioo 13279 df-icc 13282 df-fz 13438 df-fzo 13585 df-seq 13939 df-exp 13999 df-hash 14268 df-cj 15036 df-re 15037 df-im 15038 df-sqrt 15172 df-abs 15173 df-struct 17088 df-sets 17105 df-slot 17123 df-ndx 17135 df-base 17151 df-ress 17172 df-plusg 17204 df-mulr 17205 df-starv 17206 df-sca 17207 df-vsca 17208 df-ip 17209 df-tset 17210 df-ple 17211 df-ds 17213 df-unif 17214 df-hom 17215 df-cco 17216 df-rest 17356 df-topn 17357 df-0g 17375 df-gsum 17376 df-topgen 17377 df-pt 17378 df-prds 17381 df-xrs 17437 df-qtop 17442 df-imas 17443 df-xps 17445 df-mre 17519 df-mrc 17520 df-acs 17522 df-mgm 18579 df-sgrp 18658 df-mnd 18674 df-submnd 18723 df-mulg 19015 df-cntz 19263 df-cmn 19728 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-cnfld 21327 df-top 22855 df-topon 22872 df-topsp 22894 df-bases 22907 df-cld 22980 df-cls 22982 df-cn 23188 df-cnp 23189 df-haus 23276 df-cmp 23348 df-tx 23523 df-hmeo 23716 df-xms 24281 df-ms 24282 df-tms 24283 df-cncf 24844

This theorem is referenced by: cnllycmp 24928 cncmet 25295 ftalem3 27058

W3C validator