Metamath Proof Explorer

Theorem reconnlem1

Description: Lemma for reconn . Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion reconnlem1 
|- ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> ( X [,] Y ) C_ A )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> ( ( topGen ` ran (,) ) |`t A ) e. Conn )
2 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
3 2 a1i 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
4 simplll 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> A C_ RR )
5 iooretop 
 |-  ( -oo (,) z ) e. ( topGen ` ran (,) )
6 5 a1i 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( -oo (,) z ) e. ( topGen ` ran (,) ) )
7 iooretop 
 |-  ( z (,) +oo ) e. ( topGen ` ran (,) )
8 7 a1i 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z (,) +oo ) e. ( topGen ` ran (,) ) )
9 simplrl 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> X e. A )
10 4 9 sseldd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> X e. RR )
11 10 mnfltd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -oo < X )
12 eldifn 
 |-  ( z e. ( ( X [,] Y ) \ A ) -> -. z e. A )
13 12 adantl 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -. z e. A )
14 eleq1 
 |-  ( X = z -> ( X e. A <-> z e. A ) )
15 9 14 syl5ibcom 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( X = z -> z e. A ) )
16 13 15 mtod 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -. X = z )
17 eldifi 
 |-  ( z e. ( ( X [,] Y ) \ A ) -> z e. ( X [,] Y ) )
18 17 adantl 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z e. ( X [,] Y ) )
19 simplrr 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> Y e. A )
20 4 19 sseldd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> Y e. RR )
21 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( z e. ( X [,] Y ) <-> ( z e. RR /\ X <_ z /\ z <_ Y ) ) )
22 10 20 21 syl2anc 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z e. ( X [,] Y ) <-> ( z e. RR /\ X <_ z /\ z <_ Y ) ) )
23 18 22 mpbid 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z e. RR /\ X <_ z /\ z <_ Y ) )
24 23 simp2d 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> X <_ z )
25 23 simp1d 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z e. RR )
26 10 25 leloed 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( X <_ z <-> ( X < z \/ X = z ) ) )
27 24 26 mpbid 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( X < z \/ X = z ) )
28 27 ord 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( -. X < z -> X = z ) )
29 16 28 mt3d 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> X < z )
30 mnfxr 
 |-  -oo e. RR*
31 25 rexrd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z e. RR* )
32 elioo2 
 |-  ( ( -oo e. RR* /\ z e. RR* ) -> ( X e. ( -oo (,) z ) <-> ( X e. RR /\ -oo < X /\ X < z ) ) )
33 30 31 32 sylancr 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( X e. ( -oo (,) z ) <-> ( X e. RR /\ -oo < X /\ X < z ) ) )
34 10 11 29 33 mpbir3and 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> X e. ( -oo (,) z ) )
35 inelcm 
 |-  ( ( X e. ( -oo (,) z ) /\ X e. A ) -> ( ( -oo (,) z ) i^i A ) =/= (/) )
36 34 9 35 syl2anc 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( ( -oo (,) z ) i^i A ) =/= (/) )
37 eleq1 
 |-  ( z = Y -> ( z e. A <-> Y e. A ) )
38 19 37 syl5ibrcom 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z = Y -> z e. A ) )
39 13 38 mtod 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -. z = Y )
40 23 simp3d 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z <_ Y )
41 25 20 leloed 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z <_ Y <-> ( z < Y \/ z = Y ) ) )
42 40 41 mpbid 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z < Y \/ z = Y ) )
43 42 ord 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( -. z < Y -> z = Y ) )
44 39 43 mt3d 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z < Y )
45 20 ltpnfd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> Y < +oo )
46 pnfxr 
 |-  +oo e. RR*
47 elioo2 
 |-  ( ( z e. RR* /\ +oo e. RR* ) -> ( Y e. ( z (,) +oo ) <-> ( Y e. RR /\ z < Y /\ Y < +oo ) ) )
48 31 46 47 sylancl 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( Y e. ( z (,) +oo ) <-> ( Y e. RR /\ z < Y /\ Y < +oo ) ) )
49 20 44 45 48 mpbir3and 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> Y e. ( z (,) +oo ) )
50 inelcm 
 |-  ( ( Y e. ( z (,) +oo ) /\ Y e. A ) -> ( ( z (,) +oo ) i^i A ) =/= (/) )
51 49 19 50 syl2anc 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( ( z (,) +oo ) i^i A ) =/= (/) )
52 inss1 
 |-  ( ( ( -oo (,) z ) i^i ( z (,) +oo ) ) i^i A ) C_ ( ( -oo (,) z ) i^i ( z (,) +oo ) )
53 31 30 jctil 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( -oo e. RR* /\ z e. RR* ) )
54 31 46 jctir 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( z e. RR* /\ +oo e. RR* ) )
55 25 leidd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z <_ z )
56 ioodisj 
 |-  ( ( ( ( -oo e. RR* /\ z e. RR* ) /\ ( z e. RR* /\ +oo e. RR* ) ) /\ z <_ z ) -> ( ( -oo (,) z ) i^i ( z (,) +oo ) ) = (/) )
57 53 54 55 56 syl21anc 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( ( -oo (,) z ) i^i ( z (,) +oo ) ) = (/) )
58 sseq0 
 |-  ( ( ( ( ( -oo (,) z ) i^i ( z (,) +oo ) ) i^i A ) C_ ( ( -oo (,) z ) i^i ( z (,) +oo ) ) /\ ( ( -oo (,) z ) i^i ( z (,) +oo ) ) = (/) ) -> ( ( ( -oo (,) z ) i^i ( z (,) +oo ) ) i^i A ) = (/) )
59 52 57 58 sylancr 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( ( ( -oo (,) z ) i^i ( z (,) +oo ) ) i^i A ) = (/) )
60 30 a1i 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -oo e. RR* )
61 46 a1i 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> +oo e. RR* )
62 25 mnfltd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -oo < z )
63 25 ltpnfd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> z < +oo )
64 ioojoin 
 |-  ( ( ( -oo e. RR* /\ z e. RR* /\ +oo e. RR* ) /\ ( -oo < z /\ z < +oo ) ) -> ( ( ( -oo (,) z ) u. { z } ) u. ( z (,) +oo ) ) = ( -oo (,) +oo ) )
65 60 31 61 62 63 64 syl32anc 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( ( ( -oo (,) z ) u. { z } ) u. ( z (,) +oo ) ) = ( -oo (,) +oo ) )
66 unass 
 |-  ( ( ( -oo (,) z ) u. { z } ) u. ( z (,) +oo ) ) = ( ( -oo (,) z ) u. ( { z } u. ( z (,) +oo ) ) )
67 un12 
 |-  ( ( -oo (,) z ) u. ( { z } u. ( z (,) +oo ) ) ) = ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) )
68 66 67 eqtri 
 |-  ( ( ( -oo (,) z ) u. { z } ) u. ( z (,) +oo ) ) = ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) )
69 ioomax 
 |-  ( -oo (,) +oo ) = RR
70 65 68 69 3eqtr3g 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) = RR )
71 4 70 sseqtrrd 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> A C_ ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) )
72 disjsn 
 |-  ( ( A i^i { z } ) = (/) <-> -. z e. A )
73 13 72 sylibr 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( A i^i { z } ) = (/) )
74 disjssun 
 |-  ( ( A i^i { z } ) = (/) -> ( A C_ ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) <-> A C_ ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) )
75 73 74 syl 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> ( A C_ ( { z } u. ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) <-> A C_ ( ( -oo (,) z ) u. ( z (,) +oo ) ) ) )
76 71 75 mpbid 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> A C_ ( ( -oo (,) z ) u. ( z (,) +oo ) ) )
77 3 4 6 8 36 51 59 76 nconnsubb 
 |-  ( ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) /\ z e. ( ( X [,] Y ) \ A ) ) -> -. ( ( topGen ` ran (,) ) |`t A ) e. Conn )
78 77 ex 
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> ( z e. ( ( X [,] Y ) \ A ) -> -. ( ( topGen ` ran (,) ) |`t A ) e. Conn ) )
79 1 78 mt2d 
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> -. z e. ( ( X [,] Y ) \ A ) )
80 79 eq0rdv 
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> ( ( X [,] Y ) \ A ) = (/) )
81 ssdif0 
 |-  ( ( X [,] Y ) C_ A <-> ( ( X [,] Y ) \ A ) = (/) )
82 80 81 sylibr 
 |-  ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) |`t A ) e. Conn ) /\ ( X e. A /\ Y e. A ) ) -> ( X [,] Y ) C_ A )