Metamath Proof Explorer

Theorem cnllysconn

Description: The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypothesis cnllysconn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion cnllysconn 𝐽 ∈ Locally SConn

Proof

Step Hyp Ref Expression
1 cnllysconn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 1 cnfldtop ⊢ 𝐽 ∈ Top
3 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
4 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
5 4 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
6 3 5 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
7 3 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
8 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
9 simpll ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐽 )
10 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ ℂ )
11 8 9 10 sylancr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ ℂ )
12 simplr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
13 11 12 sseldd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ ℂ )
14 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
15 14 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑟 ∈ ℝ* )
16 4 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
17 7 13 15 16 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
18 simprr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
19 vex ⊢ 𝑥 ∈ V
20 19 elpw2 ⊢ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝒫 𝑥 ↔ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
21 18 20 sylibr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝒫 𝑥 )
22 17 21 elind ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ ( 𝐽 ∩ 𝒫 𝑥 ) )
23 simprl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑟 ∈ ℝ+ )
24 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
25 7 13 23 24 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
26 eqid ⊢ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) = ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 )
27 eqid ⊢ ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) = ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
28 1 26 27 blsconn ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑟 ∈ ℝ* ) → ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ SConn )
29 13 15 28 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ SConn )
30 eleq2 ⊢ ( 𝑢 = ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
31 oveq2 ⊢ ( 𝑢 = ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( 𝐽 ↾t 𝑢 ) = ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
32 31 eleq1d ⊢ ( 𝑢 = ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ( 𝐽 ↾t 𝑢 ) ∈ SConn ↔ ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ SConn ) )
33 30 32 anbi12d ⊢ ( 𝑢 = ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn ) ↔ ( 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ SConn ) ) )
34 33 rspcev ⊢ ( ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ ( 𝐽 ↾t ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ SConn ) ) → ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn ) )
35 22 25 29 34 syl12anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn ) )
36 6 35 rexlimddv ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn ) )
37 36 rgen2 ⊢ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn )
38 islly ⊢ ( 𝐽 ∈ Locally SConn ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ SConn ) ) )
39 2 37 38 mpbir2an ⊢ 𝐽 ∈ Locally SConn