Metamath Proof Explorer


Theorem reconn

Description: A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion reconn ( 𝐴 ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reconnlem1 ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
2 1 ralrimivva ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
3 2 ex ( 𝐴 ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )
4 n0 ( ( 𝑢𝐴 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝑢𝐴 ) )
5 n0 ( ( 𝑣𝐴 ) ≠ ∅ ↔ ∃ 𝑐 𝑐 ∈ ( 𝑣𝐴 ) )
6 4 5 anbi12i ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ) ↔ ( ∃ 𝑏 𝑏 ∈ ( 𝑢𝐴 ) ∧ ∃ 𝑐 𝑐 ∈ ( 𝑣𝐴 ) ) )
7 exdistrv ( ∃ 𝑏𝑐 ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ↔ ( ∃ 𝑏 𝑏 ∈ ( 𝑢𝐴 ) ∧ ∃ 𝑐 𝑐 ∈ ( 𝑣𝐴 ) ) )
8 simplll ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝐴 ⊆ ℝ )
9 simprll ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑏 ∈ ( 𝑢𝐴 ) )
10 9 elin2d ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑏𝐴 )
11 8 10 sseldd ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑏 ∈ ℝ )
12 simprlr ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑐 ∈ ( 𝑣𝐴 ) )
13 12 elin2d ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑐𝐴 )
14 8 13 sseldd ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → 𝑐 ∈ ℝ )
15 8 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝐴 ⊆ ℝ )
16 simplrl ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → 𝑢 ∈ ( topGen ‘ ran (,) ) )
17 16 ad2antrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝑢 ∈ ( topGen ‘ ran (,) ) )
18 simplrr ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → 𝑣 ∈ ( topGen ‘ ran (,) ) )
19 18 ad2antrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝑣 ∈ ( topGen ‘ ran (,) ) )
20 simpllr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
21 9 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝑏 ∈ ( 𝑢𝐴 ) )
22 12 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝑐 ∈ ( 𝑣𝐴 ) )
23 simplrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) )
24 simpr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → 𝑏𝑐 )
25 eqid sup ( ( 𝑢 ∩ ( 𝑏 [,] 𝑐 ) ) , ℝ , < ) = sup ( ( 𝑢 ∩ ( 𝑏 [,] 𝑐 ) ) , ℝ , < )
26 15 17 19 20 21 22 23 24 25 reconnlem2 ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑏𝑐 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) )
27 8 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝐴 ⊆ ℝ )
28 18 ad2antrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝑣 ∈ ( topGen ‘ ran (,) ) )
29 16 ad2antrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝑢 ∈ ( topGen ‘ ran (,) ) )
30 simpllr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
31 12 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝑐 ∈ ( 𝑣𝐴 ) )
32 9 adantr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝑏 ∈ ( 𝑢𝐴 ) )
33 incom ( 𝑣𝑢 ) = ( 𝑢𝑣 )
34 simplrr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) )
35 33 34 eqsstrid ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → ( 𝑣𝑢 ) ⊆ ( ℝ ∖ 𝐴 ) )
36 simpr ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → 𝑐𝑏 )
37 eqid sup ( ( 𝑣 ∩ ( 𝑐 [,] 𝑏 ) ) , ℝ , < ) = sup ( ( 𝑣 ∩ ( 𝑐 [,] 𝑏 ) ) , ℝ , < )
38 27 28 29 30 31 32 35 36 37 reconnlem2 ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → ¬ 𝐴 ⊆ ( 𝑣𝑢 ) )
39 uncom ( 𝑣𝑢 ) = ( 𝑢𝑣 )
40 39 sseq2i ( 𝐴 ⊆ ( 𝑣𝑢 ) ↔ 𝐴 ⊆ ( 𝑢𝑣 ) )
41 38 40 sylnib ( ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) ∧ 𝑐𝑏 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) )
42 11 14 26 41 lecasei ( ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) ∧ ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) )
43 42 exp32 ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) → ( ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
44 43 exlimdvv ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ∃ 𝑏𝑐 ( 𝑏 ∈ ( 𝑢𝐴 ) ∧ 𝑐 ∈ ( 𝑣𝐴 ) ) → ( ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
45 7 44 syl5bir ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( ∃ 𝑏 𝑏 ∈ ( 𝑢𝐴 ) ∧ ∃ 𝑐 𝑐 ∈ ( 𝑣𝐴 ) ) → ( ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
46 6 45 syl5bi ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ) → ( ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
47 46 expd ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( 𝑢𝐴 ) ≠ ∅ → ( ( 𝑣𝐴 ) ≠ ∅ → ( ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) ) )
48 47 3impd ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) )
49 48 ex ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) → ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 → ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
50 49 ralrimdvva ( 𝐴 ⊆ ℝ → ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 → ∀ 𝑢 ∈ ( topGen ‘ ran (,) ) ∀ 𝑣 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
51 retopon ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
52 connsub ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ 𝐴 ⊆ ℝ ) → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑢 ∈ ( topGen ‘ ran (,) ) ∀ 𝑣 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
53 51 52 mpan ( 𝐴 ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑢 ∈ ( topGen ‘ ran (,) ) ∀ 𝑣 ∈ ( topGen ‘ ran (,) ) ( ( ( 𝑢𝐴 ) ≠ ∅ ∧ ( 𝑣𝐴 ) ≠ ∅ ∧ ( 𝑢𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) ) → ¬ 𝐴 ⊆ ( 𝑢𝑣 ) ) ) )
54 50 53 sylibrd ( 𝐴 ⊆ ℝ → ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 → ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) )
55 3 54 impbid ( 𝐴 ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )