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 25303

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 25130	. . . 4 ⊢ 𝐽 ∈ Haus
3		simpl 488	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆ ℂ)
4		cnheibor.3	. . . . 5 ⊢ 𝑇 = (𝐽 ↾_t 𝑋)
5		simpr 490	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp)
6	4, 5	eqeltrrid 2869	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾_t 𝑋) ∈ Comp)
7	1	cnfldtopon 25128	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
8	7	toponunii 23261	. . . . 5 ⊢ ℂ = ∪ 𝐽
9	8	hauscmp 23752	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾_t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
10	2, 3, 6, 9	mp3an2i 1496	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽))
11	1	cnfldtop 25129	. . . . . . . . . . 11 ⊢ 𝐽 ∈ Top
12	8	restuni 23507	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
13	11, 3, 12	sylancr 599	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ (𝐽 ↾_t 𝑋))
14	4	unieqi 4882	. . . . . . . . . 10 ⊢ ∪ 𝑇 = ∪ (𝐽 ↾_t 𝑋)
15	13, 14	eqtr4di 2816	. . . . . . . . 9 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪ 𝑇)
16	15	eleq2d 2850	. . . . . . . 8 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇))
17	16	biimpar 483	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → 𝑥 ∈ 𝑋)
18		cnex 11305	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
19		ssexg 5285	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
20	3, 18, 19	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V)
21	20	adantr 486	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V)
22		cnxmet 25118	. . . . . . . . . . 11 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
23		0cnd 11323	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ)
24	3	sselda 3913	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ)
25	24	abscld 15632	. . . . . . . . . . . . 13 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
26		peano2re 11507	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
27	25, 26	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ)
28	27	rexrd 11383	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ^*)
29	1	cnfldtopn 25127	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
30	29	blopn 24846	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
31	22, 23, 28, 30	mp3an2i 1496	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽)
32		elrestr 17625	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
33	11, 21, 31, 32	mp3an2i 1496	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ (𝐽 ↾_t 𝑋))
34	33, 4	eleqtrrdi 2875	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇)
35		0cn 11322	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
36		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 25116	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
38	35, 37	mpan 703	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥)))
39		df-neg 11568	. . . . . . . . . . . . . . 15 ⊢ -𝑥 = (0 − 𝑥)
40	39	fveq2i 6908	. . . . . . . . . . . . . 14 ⊢ (abs‘ -𝑥) = (abs‘(0 − 𝑥))
41		absneg 15470	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (abs‘ -𝑥) = (abs‘𝑥))
42	40, 41	eqtr3id 2812	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(0 − 𝑥)) = (abs‘𝑥))
43	38, 42	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (0(abs ∘ − )𝑥) = (abs‘𝑥))
44	24, 43	syl 18	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
45	25	ltp1d 12271	. . . . . . . . . . 11 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1))
46	44, 45	eqbrtrd 5130	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))
47		elbl 24734	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ ((abs‘𝑥) + 1) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
48	22, 23, 28, 47	mp3an2i 1496	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1))))
49	24, 46, 48	mpbir2and 726	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
50		simpr 490	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
51	49, 50	elind 4100	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
52	24	absge0d 15640	. . . . . . . . . 10 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
53	25, 52	ge0p1rpd 13218	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ⁺)
54		eqid 2763	. . . . . . . . 9 ⊢ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)
55		oveq2 7448	. . . . . . . . . . 11 ⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)))
56	55	ineq1d 4119	. . . . . . . . . 10 ⊢ (𝑟 = ((abs‘𝑥) + 1) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋))
57	56	rspceeqv 3602	. . . . . . . . 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 598	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))
59		eleq2 2853	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)))
60		eqeq1 2767	. . . . . . . . . . 11 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
61	60	rexbidv 3190	. . . . . . . . . 10 ⊢ (𝑢 = ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ⁺ ((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
62	59, 61	anbi12d 644	. . . . . . . . 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 3580	. . . . . . . 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 850	. . . . . . 7 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
65	17, 64	syldan 603	. . . . . 6 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
66	65	ralrimiva 3158	. . . . 5 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)))
67		eqid 2763	. . . . . 6 ⊢ ∪ 𝑇 = ∪ 𝑇
68		oveq2 7448	. . . . . . . 8 ⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ − ))𝑟) = (0(ball‘(abs ∘ − ))(𝑓‘𝑢)))
69	68	ineq1d 4119	. . . . . . 7 ⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
70	69	eqeq2d 2774	. . . . . 6 ⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)))
71	67, 70	cmpcovf 23736	. . . . 5 ⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ⁺ 𝑢 = ((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
72	5, 66, 71	syl2anc 596	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))))
73	15	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇)
74		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪ 𝑠)
75	73, 74	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠)
76	75	eleq2d 2850	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠))
77		eluni2 4874	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑠 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)
78	76, 77	bitrdi 290	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧))
79		elssuni 4902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠)
80	79	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑠)
81	75	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 = ∪ 𝑠)
82	80, 81	sseqtrrd 3950	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
83		simp-6l 799	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ)
84	82, 83	sstrd 3923	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ)
85		simprr 785	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
86	84, 85	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ)
87	86	abscld 15632	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ)
88		simplrl 789	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ)
89		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ⁺)
90	89	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ⁺)
91		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠)
92	90, 91	ffvelcdmd 7106	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ⁺)
93	92	rpred 13188	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ)
94	86, 43	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) = (abs‘𝑥))
95		id 23	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
96		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧))
97	96	oveq2d 7456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ − ))(𝑓‘𝑢)) = (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
98	97	ineq1d 4119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
99	95, 98	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋)))
100		simprr 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
101	100	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))
102	99, 101, 91	rspcdva 3581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
103	85, 102	eleqtrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋))
104	103	elin1d 4104	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)))
105		0cnd 11323	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ)
106	92	rpxrd 13189	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ^*)
107		elbl 24734	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (𝑓‘𝑧) ∈ ℝ^*) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
108	22, 105, 106, 107	mp3an2i 1496	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧))))
109	104, 108	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ ℂ ∧ (0(abs ∘ − )𝑥) < (𝑓‘𝑧)))
110	109	simprd 501	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) < (𝑓‘𝑧))
111	94, 110	eqbrtrrd 5132	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧))
112	96	breq1d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟))
113		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
114	112, 113, 91	rspcdva 3581	. . . . . . . . . . . . . 14 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟)
115	87, 93, 88, 111, 114	ltletrd 11494	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟)
116	87, 88, 115	ltled 11482	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟)
117	116	rexlimdvaa 3168	. . . . . . . . . . 11 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟))
118	78, 117	sylbid 243	. . . . . . . . . 10 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟))
119	118	ralrimiv 3157	. . . . . . . . 9 ⊢ ((((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
120		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin))
121	120	elin2d 4105	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin)
122		ffvelcdm 7102	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ⁺)
123	122	rpred 13188	. . . . . . . . . . . 12 ⊢ ((𝑓:𝑠⟶ℝ⁺ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ)
124	123	ralrimiva 3158	. . . . . . . . . . 11 ⊢ (𝑓:𝑠⟶ℝ⁺ → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
125	124	ad2antrl 741	. . . . . . . . . 10 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ)
126		fimaxre3 12287	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
127	121, 125, 126	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)
128	119, 127	reximddv 3182	. . . . . . . 8 ⊢ (((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
129	128	ex 418	. . . . . . 7 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → ((𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
130	129	exlimdv 1968	. . . . . 6 ⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 = ∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
131	130	expimpd 459	. . . . 5 ⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
132	131	rexlimdva 3167	. . . 4 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ⁺ ∧ ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ − ))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
133	72, 132	mpd 16	. . 3 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)
134	10, 133	jca 521	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))
135		eqid 2763	. . . . . 6 ⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧)))
136		eqid 2763	. . . . . 6 ⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ (( -𝑟[,]𝑟) × ( -𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ (( -𝑟[,]𝑟) × ( -𝑟[,]𝑟)))
137	1, 4, 135, 136	cnheiborlem 25302	. . . . 5 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
138	137	rexlimdvaa 3168	. . . 4 ⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp))
139	138	imp 412	. . 3 ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp)
140	139	adantl 487	. 2 ⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp)
141	134, 140	impbida 813	1 ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∩ cin 4092 𝒫 cpw 4560 ∪ cuni 4870 class class class wbr 5106 × cxp 5653 “ cima 5658 ∘ ccom 5659 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 ∈ cmpo 7442 Fincfn 8998 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 ici 11226 + caddc 11227 · cmul 11229 ℝ^*cxr 11366 < clt 11367 ≤ cle 11368 − cmin 11565 -cneg 11566 ℝ⁺crp 13144 [,]cicc 13503 abscabs 15427 ↾_t crest 17617 TopOpenctopn 17618 ∞Metcxmet 21690 ballcbl 21692 ℂ_fldccnfld 21705 Topctop 23238 Clsdccld 23361 Hauscha 23653 Compccmp 23731

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302 ax-addf 11303

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-er 8742 df-map 8874 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-fi 9427 df-sup 9458 df-inf 9459 df-oi 9528 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-z 12718 df-dec 12839 df-uz 12990 df-q 13100 df-rp 13145 df-xneg 13265 df-xadd 13266 df-xmul 13267 df-ioo 13504 df-icc 13507 df-fz 13664 df-fzo 13813 df-seq 14169 df-exp 14229 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-starv 17469 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-unif 17477 df-hom 17478 df-cco 17479 df-rest 17619 df-topn 17620 df-0g 17638 df-gsum 17639 df-topgen 17640 df-pt 17641 df-prds 17644 df-xrs 17700 df-qtop 17705 df-imas 17706 df-xps 17708 df-mre 17782 df-mrc 17783 df-acs 17785 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-submnd 19005 df-mulg 19304 df-cntz 19558 df-cmn 20023 df-psmet 21697 df-xmet 21698 df-met 21699 df-bl 21700 df-mopn 21701 df-cnfld 21706 df-top 23239 df-topon 23256 df-topsp 23278 df-bases 23291 df-cld 23364 df-cls 23366 df-cn 23572 df-cnp 23573 df-haus 23660 df-cmp 23732 df-tx 23908 df-hmeo 24101 df-xms 24666 df-ms 24667 df-tms 24668 df-cncf 25226

This theorem is used by: cnllycmp 25304 cncmet 25670 ftalem3 27429

W3C validator