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 24987

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 24805	. . . 4 ⊢ 𝐽 ∈ Haus
3		simpl 482	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆ ℂ)
4		cnheibor.3	. . . . 5 ⊢ 𝑇 = (𝐽 ↾_t 𝑋)
5		simpr 484	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp)
6	4, 5	eqeltrrid 2846	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾_t 𝑋) ∈ Comp)
7	1	cnfldtopon 24803	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
8	7	toponunii 22922	. . . . 5 ⊢ ℂ = ∪ 𝐽
9	8	hauscmp 23415	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾_t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
10	2, 3, 6, 9	mp3an2i 1468	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
11	1	cnfldtop 24804	. . . . . . . . . . 11 ⊢ 𝐽 ∈ Top
12	8	restuni 23170	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
13	11, 3, 12	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
14	4	unieqi 4919	. . . . . . . . . 10 ⊢ ∪ 𝑇 = ∪ (𝐽 ↾_t 𝑋)
15	13, 14	eqtr4di 2795	. . . . . . . . 9 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ 𝑇)
16	15	eleq2d 2827	. . . . . . . 8 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇))
17	16	biimpar 477	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → 𝑥 ∈ 𝑋)
18		cnex 11236	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
19		ssexg 5323	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
20	3, 18, 19	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V)
21	20	adantr 480	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V)
22		cnxmet 24793	. . . . . . . . . . 11 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
23		0cnd 11254	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ)
24	3	sselda 3983	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ)
25	24	abscld 15475	. . . . . . . . . . . . 13 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
26		peano2re 11434	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
27	25, 26	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ)
28	27	rexrd 11311	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ^*)
29	1	cnfldtopn 24802	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
30	29	blopn 24513	. . . . . . . . . . 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 17473	. . . . . . . . . 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 2852	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇)
35		0cn 11253	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
36		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24791	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
38	35, 37	mpan 690	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
39		df-neg 11495	. . . . . . . . . . . . . . 15 ⊢ -𝑥 = (0 − 𝑥)
40	39	fveq2i 6909	. . . . . . . . . . . . . 14 ⊢ (abs‘-𝑥) = (abs‘(0 − 𝑥))
41		absneg 15316	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (abs‘-𝑥) = (abs‘𝑥))
42	40, 41	eqtr3id 2791	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(0 − 𝑥)) = (abs‘𝑥))
43	38, 42	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘𝑥))
44	24, 43	syl 17	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
45	25	ltp1d 12198	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1))
46	44, 45	eqbrtrd 5165	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))
47		elbl 24398	. . . . . . . . . . 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 4200	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
52	24	absge0d 15483	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
53	25, 52	ge0p1rpd 13107	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ⁺)
54		eqid 2737	. . . . . . . . 9 ⊢ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)
55		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
56	55	ineq1d 4219	. . . . . . . . . 10 ⊢ (𝑟 = ((abs‘𝑥) + 1) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
57	56	rspceeqv 3645	. . . . . . . . 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 2830	. . . . . . . . . 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 3179	. . . . . . . . . 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 3622	. . . . . . . 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 591	. . . . . 6 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
66	65	ralrimiva 3146	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
67		eqid 2737	. . . . . 6 ⊢ ∪ 𝑇 = ∪ 𝑇
68		oveq2 7439	. . . . . . . 8 ⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))(𝑓‘𝑢)))
69	68	ineq1d 4219	. . . . . . 7 ⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
70	69	eqeq2d 2748	. . . . . 6 ⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)))
71	67, 70	cmpcovf 23399	. . . . 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 776	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪ 𝑠)
75	73, 74	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠)
76	75	eleq2d 2827	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠))
77		eluni2 4911	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑠 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)
78	76, 77	bitrdi 287	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧))
79		elssuni 4937	. . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
83		simp-6l 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ)
84	82, 83	sstrd 3994	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ)
85		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
86	84, 85	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ)
87	86	abscld 15475	. . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ⁺)
91		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠)
92	90, 91	ffvelcdmd 7105	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ⁺)
93	92	rpred 13077	. . . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
97	96	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ − ))(𝑓‘𝑢)) = (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
98	97	ineq1d 4219	. . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
102	99, 101, 91	rspcdva 3623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
103	85, 102	eleqtrd 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
104	103	elin1d 4204	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
105		0cnd 11254	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ)
106	92	rpxrd 13078	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ^*)
107		elbl 24398	. . . . . . . . . . . . . . . . . 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 5167	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧))
112	96	breq1d 5153	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟))
113		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
114	112, 113, 91	rspcdva 3623	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟)
115	87, 93, 88, 111, 114	ltletrd 11421	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟)
116	87, 88, 115	ltled 11409	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟)
117	116	rexlimdvaa 3156	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟))
118	78, 117	sylbid 240	. . . . . . . . . 10 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟))
119	118	ralrimiv 3145	. . . . . . . . 9 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
120		simpllr 776	. . . . . . . . . . 11 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin))
121	120	elin2d 4205	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin)
122		ffvelcdm 7101	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ⁺)
123	122	rpred 13077	. . . . . . . . . . . 12 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ)
124	123	ralrimiva 3146	. . . . . . . . . . 11 ⊢ (𝑓:𝑠⟶ℝ⁺ → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
125	124	ad2antrl 728	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
126		fimaxre3 12214	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
127	121, 125, 126	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
128	119, 127	reximddv 3171	. . . . . . . 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 3155	. . . 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 24986	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
138	137	rexlimdvaa 3156	. . . 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 1540 ∃wex 1779 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∩ cin 3950 ⊆ wss 3951 𝒫 cpw 4600 ∪ cuni 4907 class class class wbr 5143 × cxp 5683 “ cima 5688 ∘ ccom 5689 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ∈ cmpo 7433 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 ici 11157 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 -cneg 11493 ℝ⁺crp 13034 [,]cicc 13390 abscabs 15273 ↾_t crest 17465 TopOpenctopn 17466 ∞Metcxmet 21349 ballcbl 21351 ℂ_fldccnfld 21364 Topctop 22899 Clsdccld 23024 Hauscha 23316 Compccmp 23394

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-map 8868 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-icc 13394 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-cls 23029 df-cn 23235 df-cnp 23236 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904

This theorem is referenced by: cnllycmp 24988 cncmet 25356 ftalem3 27118

W3C validator