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
|- ( A C_ RR -> ( ( ( topGen ` ran (,) ) |`t A ) e. Conn <-> A. x e. A A. y e. A ( x [,] y ) C_ A ) )

Proof

Step Hyp Ref Expression
1 reconnlem1
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( x e. A /\ y e. A ) ) -> ( x [,] y ) C_ A )
2 1 ralrimivva
 |-  ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) -> A. x e. A A. y e. A ( x [,] y ) C_ A )
3 2 ex
 |-  ( A C_ RR -> ( ( ( topGen ` ran (,) ) |`t A ) e. Conn -> A. x e. A A. y e. A ( x [,] y ) C_ A ) )
4 n0
 |-  ( ( u i^i A ) =/= (/) <-> E. b b e. ( u i^i A ) )
5 n0
 |-  ( ( v i^i A ) =/= (/) <-> E. c c e. ( v i^i A ) )
6 4 5 anbi12i
 |-  ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) ) <-> ( E. b b e. ( u i^i A ) /\ E. c c e. ( v i^i A ) ) )
7 exdistrv
 |-  ( E. b E. c ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) <-> ( E. b b e. ( u i^i A ) /\ E. c c e. ( v i^i A ) ) )
8 simplll
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> A C_ RR )
9 simprll
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> b e. ( u i^i A ) )
10 9 elin2d
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> b e. A )
11 8 10 sseldd
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> b e. RR )
12 simprlr
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> c e. ( v i^i A ) )
13 12 elin2d
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> c e. A )
14 8 13 sseldd
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> c e. RR )
15 8 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> A C_ RR )
16 simplrl
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> u e. ( topGen ` ran (,) ) )
17 16 ad2antrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> u e. ( topGen ` ran (,) ) )
18 simplrr
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> v e. ( topGen ` ran (,) ) )
19 18 ad2antrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> v e. ( topGen ` ran (,) ) )
20 simpllr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> A. x e. A A. y e. A ( x [,] y ) C_ A )
21 9 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> b e. ( u i^i A ) )
22 12 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> c e. ( v i^i A ) )
23 simplrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> ( u i^i v ) C_ ( RR \ A ) )
24 simpr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> b <_ c )
25 eqid
 |-  sup ( ( u i^i ( b [,] c ) ) , RR , < ) = sup ( ( u i^i ( b [,] c ) ) , RR , < )
26 15 17 19 20 21 22 23 24 25 reconnlem2
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ b <_ c ) -> -. A C_ ( u u. v ) )
27 8 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> A C_ RR )
28 18 ad2antrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> v e. ( topGen ` ran (,) ) )
29 16 ad2antrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> u e. ( topGen ` ran (,) ) )
30 simpllr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> A. x e. A A. y e. A ( x [,] y ) C_ A )
31 12 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> c e. ( v i^i A ) )
32 9 adantr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> b e. ( u i^i A ) )
33 incom
 |-  ( v i^i u ) = ( u i^i v )
34 simplrr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> ( u i^i v ) C_ ( RR \ A ) )
35 33 34 eqsstrid
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> ( v i^i u ) C_ ( RR \ A ) )
36 simpr
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> c <_ b )
37 eqid
 |-  sup ( ( v i^i ( c [,] b ) ) , RR , < ) = sup ( ( v i^i ( c [,] b ) ) , RR , < )
38 27 28 29 30 31 32 35 36 37 reconnlem2
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> -. A C_ ( v u. u ) )
39 uncom
 |-  ( v u. u ) = ( u u. v )
40 39 sseq2i
 |-  ( A C_ ( v u. u ) <-> A C_ ( u u. v ) )
41 38 40 sylnib
 |-  ( ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) /\ c <_ b ) -> -. A C_ ( u u. v ) )
42 11 14 26 41 lecasei
 |-  ( ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) /\ ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) /\ ( u i^i v ) C_ ( RR \ A ) ) ) -> -. A C_ ( u u. v ) )
43 42 exp32
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) -> ( ( u i^i v ) C_ ( RR \ A ) -> -. A C_ ( u u. v ) ) ) )
44 43 exlimdvv
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( E. b E. c ( b e. ( u i^i A ) /\ c e. ( v i^i A ) ) -> ( ( u i^i v ) C_ ( RR \ A ) -> -. A C_ ( u u. v ) ) ) )
45 7 44 syl5bir
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( ( E. b b e. ( u i^i A ) /\ E. c c e. ( v i^i A ) ) -> ( ( u i^i v ) C_ ( RR \ A ) -> -. A C_ ( u u. v ) ) ) )
46 6 45 syl5bi
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) ) -> ( ( u i^i v ) C_ ( RR \ A ) -> -. A C_ ( u u. v ) ) ) )
47 46 expd
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( ( u i^i A ) =/= (/) -> ( ( v i^i A ) =/= (/) -> ( ( u i^i v ) C_ ( RR \ A ) -> -. A C_ ( u u. v ) ) ) ) )
48 47 3impd
 |-  ( ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) /\ ( u i^i v ) C_ ( RR \ A ) ) -> -. A C_ ( u u. v ) ) )
49 48 ex
 |-  ( ( A C_ RR /\ ( u e. ( topGen ` ran (,) ) /\ v e. ( topGen ` ran (,) ) ) ) -> ( A. x e. A A. y e. A ( x [,] y ) C_ A -> ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) /\ ( u i^i v ) C_ ( RR \ A ) ) -> -. A C_ ( u u. v ) ) ) )
50 49 ralrimdvva
 |-  ( A C_ RR -> ( A. x e. A A. y e. A ( x [,] y ) C_ A -> A. u e. ( topGen ` ran (,) ) A. v e. ( topGen ` ran (,) ) ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) /\ ( u i^i v ) C_ ( RR \ A ) ) -> -. A C_ ( u u. v ) ) ) )
51 retopon
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
52 connsub
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ A C_ RR ) -> ( ( ( topGen ` ran (,) ) |`t A ) e. Conn <-> A. u e. ( topGen ` ran (,) ) A. v e. ( topGen ` ran (,) ) ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) /\ ( u i^i v ) C_ ( RR \ A ) ) -> -. A C_ ( u u. v ) ) ) )
53 51 52 mpan
 |-  ( A C_ RR -> ( ( ( topGen ` ran (,) ) |`t A ) e. Conn <-> A. u e. ( topGen ` ran (,) ) A. v e. ( topGen ` ran (,) ) ( ( ( u i^i A ) =/= (/) /\ ( v i^i A ) =/= (/) /\ ( u i^i v ) C_ ( RR \ A ) ) -> -. A C_ ( u u. v ) ) ) )
54 50 53 sylibrd
 |-  ( A C_ RR -> ( A. x e. A A. y e. A ( x [,] y ) C_ A -> ( ( topGen ` ran (,) ) |`t A ) e. Conn ) )
55 3 54 impbid
 |-  ( A C_ RR -> ( ( ( topGen ` ran (,) ) |`t A ) e. Conn <-> A. x e. A A. y e. A ( x [,] y ) C_ A ) )