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 ) )