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 biimtrrid ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( topGen ‘ ran (,) ) ∧ 𝑣 ∈ ( topGen ‘ ran (,) ) ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( ( ∃ 𝑏 𝑏 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∃ 𝑐 𝑐 ∈ ( 𝑣 ∩ 𝐴 ) ) → ( ( 𝑢 ∩ 𝑣 ) ⊆ ( ℝ ∖ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
46 6 45 biimtrid ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑢 ∈ ( 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 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )