rellysconn

Description: The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	rellysconn	$⊢ topGen (ran (.)) \in LocallySConn$

Proof

Step	Hyp	Ref	Expression
1		retop	$⊢ topGen (ran (.)) \in Top$
2		tg2	$⊢ (x \in topGen (ran (.)) \land y \in x) \to \exists z \in ran (.) (y \in z \land z \subseteq x)$
3		retopbas	$⊢ ran (.) \in TopBases$
4		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
5	3 4	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
6		simprl	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to z \in ran (.)$
7	5 6	sselid	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to z \in topGen (ran (.))$
8		simprrr	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to z \subseteq x$
9		velpw	$⊢ z \in 𝒫 x \leftrightarrow z \subseteq x$
10	8 9	sylibr	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to z \in 𝒫 x$
11	7 10	elind	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to z \in (topGen (ran (.)) \cap 𝒫 x)$
12		simprrl	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to y \in z$
13		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
14		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
15		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b))$
16	13 14 15	mp2b	$⊢ z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b)$
17		oveq2	$⊢ z = (a, b) \to topGen (ran (.)) ↾_{𝑡} z = topGen (ran (.)) ↾_{𝑡} (a, b)$
18		ioosconn	$⊢ topGen (ran (.)) ↾_{𝑡} (a, b) \in SConn$
19	17 18	eqeltrdi	$⊢ z = (a, b) \to topGen (ran (.)) ↾_{𝑡} z \in SConn$
20	19	rexlimivw	$⊢ \exists b \in ℝ^{*} z = (a, b) \to topGen (ran (.)) ↾_{𝑡} z \in SConn$
21	20	rexlimivw	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b) \to topGen (ran (.)) ↾_{𝑡} z \in SConn$
22	16 21	sylbi	$⊢ z \in ran (.) \to topGen (ran (.)) ↾_{𝑡} z \in SConn$
23	22	ad2antrl	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to topGen (ran (.)) ↾_{𝑡} z \in SConn$
24	11 12 23	jca32	$⊢ ((x \in topGen (ran (.)) \land y \in x) \land (z \in ran (.) \land (y \in z \land z \subseteq x))) \to (z \in (topGen (ran (.)) \cap 𝒫 x) \land (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn))$
25	24	ex	$⊢ (x \in topGen (ran (.)) \land y \in x) \to ((z \in ran (.) \land (y \in z \land z \subseteq x)) \to (z \in (topGen (ran (.)) \cap 𝒫 x) \land (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn)))$
26	25	reximdv2	$⊢ (x \in topGen (ran (.)) \land y \in x) \to (\exists z \in ran (.) (y \in z \land z \subseteq x) \to \exists z \in (topGen (ran (.)) \cap 𝒫 x) (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn))$
27	2 26	mpd	$⊢ (x \in topGen (ran (.)) \land y \in x) \to \exists z \in (topGen (ran (.)) \cap 𝒫 x) (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn)$
28	27	rgen2	$⊢ \forall x \in topGen (ran (.)) \forall y \in x \exists z \in (topGen (ran (.)) \cap 𝒫 x) (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn)$
29		islly	$⊢ topGen (ran (.)) \in LocallySConn\leftrightarrow(topGen (ran (.)) \in Top \land \forall x \in topGen (ran (.)) \forall y \in x \exists z \in (topGen (ran (.)) \cap 𝒫 x) (y \in z \land topGen (ran (.)) ↾_{𝑡} z \in SConn))$
30	1 28 29	mpbir2an	$⊢ topGen (ran (.)) \in LocallySConn$

Metamath Proof Explorer

Theorem rellysconn

Proof