Metamath Proof Explorer

Theorem rellysconn

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

Ref Expression
Assertion rellysconn ( topGen ‘ ran (,) ) ∈ Locally SConn

Proof

Step Hyp Ref Expression
1 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
2 tg2 ⊢ ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
3 retopbas ⊢ ran (,) ∈ TopBases
4 bastg ⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
5 3 4 ax-mp ⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
6 simprl ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ∈ ran (,) )
7 5 6 sseldi ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ∈ ( topGen ‘ ran (,) ) )
8 simprrr ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ⊆ 𝑥 )
9 velpw ⊢ ( 𝑧 ∈ 𝒫 𝑥 ↔ 𝑧 ⊆ 𝑥 )
10 8 9 sylibr ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ∈ 𝒫 𝑥 )
11 7 10 elind ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) )
12 simprrl ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑦 ∈ 𝑧 )
13 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
14 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
15 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) ) )
16 13 14 15 mp2b ⊢ ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) )
17 oveq2 ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) )
18 ioosconn ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ SConn
19 17 18 eqeltrdi ⊢ ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
20 19 rexlimivw ⊢ ( ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
21 20 rexlimivw ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
22 16 21 sylbi ⊢ ( 𝑧 ∈ ran (,) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
23 22 ad2antrl ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
24 11 12 23 jca32 ⊢ ( ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn ) ) )
25 24 ex ⊢ ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑧 ∈ ran (,) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → ( 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn ) ) ) )
26 25 reximdv2 ⊢ ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn ) ) )
27 2 26 mpd ⊢ ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn ) )
28 27 rgen2 ⊢ ∀ 𝑥 ∈ ( topGen ‘ ran (,) ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn )
29 islly ⊢ ( ( topGen ‘ ran (,) ) ∈ Locally SConn ↔ ( ( topGen ‘ ran (,) ) ∈ Top ∧ ∀ 𝑥 ∈ ( topGen ‘ ran (,) ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( topGen ‘ ran (,) ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t 𝑧 ) ∈ SConn ) ) )
30 1 28 29 mpbir2an ⊢ ( topGen ‘ ran (,) ) ∈ Locally SConn