cnllysconn

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

		Ref	Expression
	Hypothesis	cnllysconn.j	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	cnllysconn	$⊢ J \in LocallySConn$

Proof

Step	Hyp	Ref	Expression
1		cnllysconn.j	$⊢ J = TopOpen (ℂ_{fld})$
2	1	cnfldtop	$⊢ J \in Top$
3		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
4	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
5	4	mopni2	$⊢ (abs \circ - \in ∞Met (ℂ) \land x \in J \land y \in x) \to \exists r \in ℝ^{+} y ball (abs \circ -) r \subseteq x$
6	3 5	mp3an1	$⊢ (x \in J \land y \in x) \to \exists r \in ℝ^{+} y ball (abs \circ -) r \subseteq x$
7	3	a1i	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to abs \circ - \in ∞Met (ℂ)$
8	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
9		simpll	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to x \in J$
10		toponss	$⊢ (J \in TopOn (ℂ) \land x \in J) \to x \subseteq ℂ$
11	8 9 10	sylancr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to x \subseteq ℂ$
12		simplr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in x$
13	11 12	sseldd	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in ℂ$
14		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
15	14	ad2antrl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to r \in ℝ^{*}$
16	4	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land r \in ℝ^{*}) \to y ball (abs \circ -) r \in J$
17	7 13 15 16	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) r \in J$
18		simprr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) r \subseteq x$
19		vex	$⊢ x \in V$
20	19	elpw2	$⊢ y ball (abs \circ -) r \in 𝒫 x \leftrightarrow y ball (abs \circ -) r \subseteq x$
21	18 20	sylibr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) r \in 𝒫 x$
22	17 21	elind	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) r \in (J \cap 𝒫 x)$
23		simprl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to r \in ℝ^{+}$
24		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land r \in ℝ^{+}) \to y \in (y ball (abs \circ -) r)$
25	7 13 23 24	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in (y ball (abs \circ -) r)$
26		eqid	$⊢ y ball (abs \circ -) r = y ball (abs \circ -) r$
27		eqid	$⊢ J ↾_{𝑡} (y ball (abs \circ -) r) = J ↾_{𝑡} (y ball (abs \circ -) r)$
28	1 26 27	blsconn	$⊢ (y \in ℂ \land r \in ℝ^{*}) \to J ↾_{𝑡} (y ball (abs \circ -) r) \in SConn$
29	13 15 28	syl2anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to J ↾_{𝑡} (y ball (abs \circ -) r) \in SConn$
30		eleq2	$⊢ u = y ball (abs \circ -) r \to (y \in u \leftrightarrow y \in (y ball (abs \circ -) r))$
31		oveq2	$⊢ u = y ball (abs \circ -) r \to J ↾_{𝑡} u = J ↾_{𝑡} (y ball (abs \circ -) r)$
32	31	eleq1d	$⊢ u = y ball (abs \circ -) r \to (J ↾_{𝑡} u \in SConn \leftrightarrow J ↾_{𝑡} (y ball (abs \circ -) r) \in SConn)$
33	30 32	anbi12d	$⊢ u = y ball (abs \circ -) r \to ((y \in u \land J ↾_{𝑡} u \in SConn) \leftrightarrow (y \in (y ball (abs \circ -) r) \land J ↾_{𝑡} (y ball (abs \circ -) r) \in SConn))$
34	33	rspcev	$⊢ (y ball (abs \circ -) r \in (J \cap 𝒫 x) \land (y \in (y ball (abs \circ -) r) \land J ↾_{𝑡} (y ball (abs \circ -) r) \in SConn)) \to \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in SConn)$
35	22 25 29 34	syl12anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in SConn)$
36	6 35	rexlimddv	$⊢ (x \in J \land y \in x) \to \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in SConn)$
37	36	rgen2	$⊢ \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in SConn)$
38		islly	$⊢ J \in LocallySConn\leftrightarrow(J \in Top \land \forall x \in J)$
39	2 37 38	mpbir2an	$⊢ J \in LocallySConn$

Metamath Proof Explorer

Theorem cnllysconn

Proof