Theorem cncfuni 46628

Description: A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
cncfuni.acn	⊢ (𝜑 → 𝐴 ⊆ ℂ)
cncfuni.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
cncfuni.auni	⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵)
cncfuni.opn	⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴))
cncfuni.fcn	⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))

Assertion

Ref	Expression
cncfuni	⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))

Distinct variable groups:   𝐴,𝑏   𝐵,𝑏   𝐹,𝑏   𝜑,𝑏

Proof of Theorem cncfuni

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncfuni.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
2		cncfuni.auni	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵)
3	2	sselda 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝐵)
4		eluni2 4875	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏)
5	3, 4	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏)
6		simp1l 1215	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝜑)
7		simp2 1154	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑏 ∈ 𝐵)
8		elin 3920	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∩ 𝑏) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏))
9	8	biimpri 231	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏))
10	9	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏))
11	10	3adant2 1148	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏))
12		cncfuni.fcn	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))
13	1	fdmd 6716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐹 = 𝐴)
14	13	ineq2d 4172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑏 ∩ dom 𝐹) = (𝑏 ∩ 𝐴))
15		incom 4161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∩ 𝐴) = (𝐴 ∩ 𝑏)
16	14, 15	eqtr2di 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴 ∩ 𝑏) = (𝑏 ∩ dom 𝐹))
17	16	reseq2d 5977	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ (𝑏 ∩ dom 𝐹)))
18		resindm 6028	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ↾ (𝑏 ∩ dom 𝐹)) = (𝐹 ↾ 𝑏)
19	17, 18	eqtrdi 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ 𝑏))
20		cncfuni.acn	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
21	20	ssinss1d 4199	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ℂ)
22		ssidd 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℂ ⊆ ℂ)
23		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
24		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏))
25	23	cnfldtop 24951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂfld) ∈ Top
26		unicntop 24953	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
27	26	restid 17492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
28	25, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
29	28	eqcomi 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
30	23, 24, 29	cncfcn 25080	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑏) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴 ∩ 𝑏)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)))
31	21, 22, 30	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴 ∩ 𝑏)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)))
32	31	eqcomd 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)) = ((𝐴 ∩ 𝑏)–cn→ℂ))
33	19, 32	eleq12d 2856	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ)))
34	33	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ)))
35	12, 34	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)))
36	35	3adant3 1149	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)))
37	23	cnfldtopon 24950	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
39		resttopon 23329	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴 ∩ 𝑏) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)))
40	38, 21, 39	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)))
41	40	3ad2ant1 1150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)))
42	37	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
43		cncnp 23448	. . . . . . . . . . . . 13 ⊢ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)) ↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))))
44	41, 42, 43	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld)) ↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))))
45	36, 44	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥)))
46	45	simprd 500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
47		simp3 1155	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈ (𝐴 ∩ 𝑏))
48		rspa 3253	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥) ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
49	46, 47, 48	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
50	25	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (TopOpen‘ℂfld) ∈ Top)
51		inss1 4188	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ 𝐴)
53		cnex 11187	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
54	53	ssex 5290	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V)
55	20, 54	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ V)
56		restabs 23333	. . . . . . . . . . . . . 14 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴 ∧ 𝐴 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)))
57	50, 52, 55, 56	syl3anc 1397	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)))
58	57	eqcomd 2768	. . . . . . . . . . . 12 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = (((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)))
59	58	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld)) = ((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld)))
60	59	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝜑 → ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
61	60	3ad2ant1 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
62	49, 61	eleqtrd 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥))
63		resttop 23328	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top)
64	50, 55, 63	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top)
65	64	3ad2ant1 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top)
66	26	restuni 23330	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ⊆ ℂ) → 𝐴 = ∪ ((TopOpen‘ℂfld) ↾t 𝐴))
67	50, 20, 66	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 = ∪ ((TopOpen‘ℂfld) ↾t 𝐴))
68	52, 67	sseqtrd 3972	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝐴))
69	68	3ad2ant1 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝐴))
70		cncfuni.opn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴))
71	70	3adant3 1149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴))
72		eqid 2762	. . . . . . . . . . . . 13 ⊢ ∪ ((TopOpen‘ℂfld) ↾t 𝐴) = ∪ ((TopOpen‘ℂfld) ↾t 𝐴)
73	72	isopn3 23234	. . . . . . . . . . . 12 ⊢ ((((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝐴)) → ((𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏)))
74	65, 69, 73	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏)))
75	71, 74	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏))
76	47, 75	eleqtrrd 2865	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)))
77	67, 1	feq2dd 6691	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:∪ ((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)
78	77	3ad2ant1 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹:∪ ((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)
79	72, 26	cnprest 23457	. . . . . . . . 9 ⊢ (((((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ ∪ ((TopOpen‘ℂfld) ↾t 𝐴)) ∧ (𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) ∧ 𝐹:∪ ((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥)))
80	65, 69, 76, 78, 79	syl22anc 851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈ (((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))‘𝑥)))
81	62, 80	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))
82	6, 7, 11, 81	syl3anc 1397	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))
83	82	rexlimdv3a 3169	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥)))
84	5, 83	mpd 16	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))
85	84	ralrimiva 3156	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))
86		resttopon 23329	. . . . 5 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴))
87	38, 20, 86	syl2anc 595	. . . 4 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴))
88		cncnp 23448	. . . 4 ⊢ ((((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))))
89	87, 38, 88	syl2anc 595	. . 3 ⊢ (𝜑 → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝐴) CnP (TopOpen‘ℂfld))‘𝑥))))
90	1, 85, 89	mpbir2and 725	. 2 ⊢ (𝜑 → 𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld)))
91		eqid 2762	. . . 4 ⊢ ((TopOpen‘ℂfld) ↾t 𝐴) = ((TopOpen‘ℂfld) ↾t 𝐴)
92	23, 91, 29	cncfcn 25080	. . 3 ⊢ ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐴–cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld)))
93	20, 22, 92	syl2anc 595	. 2 ⊢ (𝜑 → (𝐴–cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld)))
94	90, 93	eleqtrrd 2865	1 ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ∃wrex 3088  Vcvv 3454   ∩ cin 3903   ⊆ wss 3904  ∪ cuni 4871  dom cdm 5660   ↾ cres 5662  ⟶wf 6532  ‘cfv 6536  (class class class)co 7412  ℂcc 11104   ↾_t crest 17479  TopOpenctopn 17480  ℂ_fldccnfld 21533  Topctop 23061  TopOnctopon 23078  intcnt 23185   Cn ccn 23392   CnP ccnp 23393  –cn→ccncf 25046

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-er 8692  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9369  df-sup 9400  df-inf 9401  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-3 12310  df-4 12311  df-5 12312  df-6 12313  df-7 12314  df-8 12315  df-9 12316  df-n0 12511  df-z 12598  df-dec 12718  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13143  df-xadd 13144  df-xmul 13145  df-fz 13542  df-seq 14045  df-exp 14105  df-cj 15157  df-re 15158  df-im 15159  df-sqrt 15293  df-abs 15294  df-struct 17213  df-slot 17248  df-ndx 17260  df-base 17276  df-plusg 17329  df-mulr 17330  df-starv 17331  df-tset 17335  df-ple 17336  df-ds 17338  df-unif 17339  df-rest 17481  df-topn 17482  df-topgen 17502  df-psmet 21525  df-xmet 21526  df-met 21527  df-bl 21528  df-mopn 21529  df-cnfld 21534  df-top 23062  df-topon 23079  df-topsp 23101  df-bases 23114  df-ntr 23188  df-cn 23395  df-cnp 23396  df-xms 24488  df-ms 24489  df-cncf 25048

This theorem is used by:  fouriersw  46973