Theorem cncfcnvcn

Description: Rewrite cmphaushmeo for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015)

	Ref	Expression
Hypotheses	cncfcnvcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	cncfcnvcn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝑋 )
Assertion	cncfcnvcn	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cncfcnvcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cncfcnvcn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝑋 )
3		simpr	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) )
4		cncfrss	⊢ ( 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) → 𝑋 ⊆ ℂ )
5	4	adantl	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 ⊆ ℂ )
6		cncfrss2	⊢ ( 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) → 𝑌 ⊆ ℂ )
7	6	adantl	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 ⊆ ℂ )
8		eqid	⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
9	1 2 8	cncfcn	⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 –cn→ 𝑌 ) = ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
10	5 7 9	syl2anc	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝑋 –cn→ 𝑌 ) = ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
11	3 10	eleqtrd	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
12		ishmeo	⊢ ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ( 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) ∧ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
13	12	baib	⊢ ( 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
14	11 13	syl	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
15	1	cnfldtop	⊢ 𝐽 ∈ Top
16	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
17	16	toponunii	⊢ ℂ = ∪ 𝐽
18	17	restuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ ) → 𝑋 = ∪ ( 𝐽 ↾t 𝑋 ) )
19	15 5 18	sylancr	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 = ∪ ( 𝐽 ↾t 𝑋 ) )
20	2	unieqi	⊢ ∪ 𝐾 = ∪ ( 𝐽 ↾t 𝑋 )
21	19 20	eqtr4di	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 = ∪ 𝐾 )
22	21	f1oeq2d	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
23	17	restuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ℂ ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
24	15 7 23	sylancr	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
25	24	f1oeq3d	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 : 𝑋 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
26		simpl	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐾 ∈ Comp )
27	1	cnfldhaus	⊢ 𝐽 ∈ Haus
28		cnex	⊢ ℂ ∈ V
29	28	ssex	⊢ ( 𝑌 ⊆ ℂ → 𝑌 ∈ V )
30	7 29	syl	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 ∈ V )
31		resthaus	⊢ ( ( 𝐽 ∈ Haus ∧ 𝑌 ∈ V ) → ( 𝐽 ↾t 𝑌 ) ∈ Haus )
32	27 30 31	sylancr	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐽 ↾t 𝑌 ) ∈ Haus )
33		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
34		eqid	⊢ ∪ ( 𝐽 ↾t 𝑌 ) = ∪ ( 𝐽 ↾t 𝑌 )
35	33 34	cmphaushmeo	⊢ ( ( 𝐾 ∈ Comp ∧ ( 𝐽 ↾t 𝑌 ) ∈ Haus ∧ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
36	26 32 11 35	syl3anc	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
37	22 25 36	3bitr4d	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ) )
38	1 8 2	cncfcn	⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ ) → ( 𝑌 –cn→ 𝑋 ) = ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
39	7 5 38	syl2anc	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝑌 –cn→ 𝑋 ) = ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
40	39	eleq2d	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
41	14 37 40	3bitr4d	⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ) )