Metamath Proof Explorer

Theorem iccllysconn

Description: A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion iccllysconn ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Locally SConn )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑥 ∈ ( topGen ‘ ran (,) ) )
2 inss1 ⊢ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥
3 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) )
4 2 3 sselid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ 𝑥 )
5 tg2 ⊢ ( ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
6 1 4 5 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
7 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
8 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
9 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) ) )
10 7 8 9 mp2b ⊢ ( 𝑧 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) )
11 inss1 ⊢ ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑧
12 simprrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 ⊆ 𝑥 )
13 11 12 sstrid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 )
14 simprrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑦 ∈ 𝑧 )
15 simprl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → 𝑧 = ( 𝑎 (,) 𝑏 ) )
16 15 ineq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) = ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
17 16 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) )
18 ioosconn ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ SConn
19 ioossre ⊢ ( 𝑎 (,) 𝑏 ) ⊆ ℝ
20 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) )
21 20 resconn ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ SConn ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ Conn ) )
22 reconn ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ Conn ↔ ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
23 21 22 bitrd ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ SConn ↔ ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
24 19 23 ax-mp ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝑎 (,) 𝑏 ) ) ∈ SConn ↔ ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) )
25 18 24 mpbi ⊢ ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 )
26 inss1 ⊢ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝑎 (,) 𝑏 )
27 ssralv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝑎 (,) 𝑏 ) → ( ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) → ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
28 27 ralimdv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝑎 (,) 𝑏 ) → ( ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) → ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
29 ssralv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝑎 (,) 𝑏 ) → ( ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
30 28 29 syld ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝑎 (,) 𝑏 ) → ( ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ) )
31 26 30 ax-mp ⊢ ( ∀ 𝑢 ∈ ( 𝑎 (,) 𝑏 ) ∀ 𝑣 ∈ ( 𝑎 (,) 𝑏 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) )
32 25 31 mp1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) )
33 inss2 ⊢ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 )
34 iccconn ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )
35 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
36 reconn ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ↔ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
37 35 36 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ↔ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
38 34 37 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) )
39 38 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) )
40 ssralv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) → ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
41 40 ralimdv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) → ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
42 ssralv ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
43 41 42 syld ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
44 33 39 43 mpsyl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) )
45 ssin ⊢ ( ( ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
46 45 2ralbii ⊢ ( ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ↔ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
47 r19.26-2 ⊢ ( ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ↔ ( ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ∧ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
48 46 47 bitr3i ⊢ ( ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ↔ ( ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝑎 (,) 𝑏 ) ∧ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( 𝐴 [,] 𝐵 ) ) )
49 32 44 48 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
50 26 19 sstri ⊢ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ
51 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
52 51 resconn ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ↔ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ) )
53 reconn ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ↔ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) )
54 52 53 bitrd ⊢ ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ↔ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) )
55 50 54 ax-mp ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ↔ ∀ 𝑢 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑣 ∈ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ( 𝑢 [,] 𝑣 ) ⊆ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
56 49 55 sylibr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn )
57 17 56 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn )
58 13 14 57 3jca ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) ∧ ( 𝑧 = ( 𝑎 (,) 𝑏 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ) → ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) )
59 58 exp32 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) ) )
60 59 rexlimdvw ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) ) )
61 60 rexlimdvw ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑧 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) ) )
62 10 61 syl5bi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑧 ∈ ran (,) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) ) )
63 62 reximdvai ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ∃ 𝑧 ∈ ran (,) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) )
64 retopbas ⊢ ran (,) ∈ TopBases
65 bastg ⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
66 ssrexv ⊢ ( ran (,) ⊆ ( topGen ‘ ran (,) ) → ( ∃ 𝑧 ∈ ran (,) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) → ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) )
67 64 65 66 mp2b ⊢ ( ∃ 𝑧 ∈ ran (,) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) → ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) )
68 63 67 syl6 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ∃ 𝑧 ∈ ran (,) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) )
69 6 68 mpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ ( topGen ‘ ran (,) ) ∧ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) )
70 69 ralrimivva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∀ 𝑥 ∈ ( topGen ‘ ran (,) ) ∀ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) )
71 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
72 ovex ⊢ ( 𝐴 [,] 𝐵 ) ∈ V
73 subislly ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ∈ V ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Locally SConn ↔ ∀ 𝑥 ∈ ( topGen ‘ ran (,) ) ∀ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) ) )
74 71 72 73 mp2an ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Locally SConn ↔ ∀ 𝑥 ∈ ( topGen ‘ ran (,) ) ∀ 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ∃ 𝑧 ∈ ( topGen ‘ ran (,) ) ( ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑧 ∧ ( ( topGen ‘ ran (,) ) ↾t ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ) ∈ SConn ) )
75 70 74 sylibr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Locally SConn )