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 AtopGenran.𝑡AConnXAYAXYA

Proof

Step Hyp Ref Expression
1 simplr AtopGenran.𝑡AConnXAYAtopGenran.𝑡AConn
2 retopon topGenran.TopOn
3 2 a1i AtopGenran.𝑡AConnXAYAzXYAtopGenran.TopOn
4 simplll AtopGenran.𝑡AConnXAYAzXYAA
5 iooretop −∞ztopGenran.
6 5 a1i AtopGenran.𝑡AConnXAYAzXYA−∞ztopGenran.
7 iooretop z+∞topGenran.
8 7 a1i AtopGenran.𝑡AConnXAYAzXYAz+∞topGenran.
9 simplrl AtopGenran.𝑡AConnXAYAzXYAXA
10 4 9 sseldd AtopGenran.𝑡AConnXAYAzXYAX
11 10 mnfltd AtopGenran.𝑡AConnXAYAzXYA−∞<X
12 eldifn zXYA¬zA
13 12 adantl AtopGenran.𝑡AConnXAYAzXYA¬zA
14 eleq1 X=zXAzA
15 9 14 syl5ibcom AtopGenran.𝑡AConnXAYAzXYAX=zzA
16 13 15 mtod AtopGenran.𝑡AConnXAYAzXYA¬X=z
17 eldifi zXYAzXY
18 17 adantl AtopGenran.𝑡AConnXAYAzXYAzXY
19 simplrr AtopGenran.𝑡AConnXAYAzXYAYA
20 4 19 sseldd AtopGenran.𝑡AConnXAYAzXYAY
21 elicc2 XYzXYzXzzY
22 10 20 21 syl2anc AtopGenran.𝑡AConnXAYAzXYAzXYzXzzY
23 18 22 mpbid AtopGenran.𝑡AConnXAYAzXYAzXzzY
24 23 simp2d AtopGenran.𝑡AConnXAYAzXYAXz
25 23 simp1d AtopGenran.𝑡AConnXAYAzXYAz
26 10 25 leloed AtopGenran.𝑡AConnXAYAzXYAXzX<zX=z
27 24 26 mpbid AtopGenran.𝑡AConnXAYAzXYAX<zX=z
28 27 ord AtopGenran.𝑡AConnXAYAzXYA¬X<zX=z
29 16 28 mt3d AtopGenran.𝑡AConnXAYAzXYAX<z
30 mnfxr −∞*
31 25 rexrd AtopGenran.𝑡AConnXAYAzXYAz*
32 elioo2 −∞*z*X−∞zX−∞<XX<z
33 30 31 32 sylancr AtopGenran.𝑡AConnXAYAzXYAX−∞zX−∞<XX<z
34 10 11 29 33 mpbir3and AtopGenran.𝑡AConnXAYAzXYAX−∞z
35 inelcm X−∞zXA−∞zA
36 34 9 35 syl2anc AtopGenran.𝑡AConnXAYAzXYA−∞zA
37 eleq1 z=YzAYA
38 19 37 syl5ibrcom AtopGenran.𝑡AConnXAYAzXYAz=YzA
39 13 38 mtod AtopGenran.𝑡AConnXAYAzXYA¬z=Y
40 23 simp3d AtopGenran.𝑡AConnXAYAzXYAzY
41 25 20 leloed AtopGenran.𝑡AConnXAYAzXYAzYz<Yz=Y
42 40 41 mpbid AtopGenran.𝑡AConnXAYAzXYAz<Yz=Y
43 42 ord AtopGenran.𝑡AConnXAYAzXYA¬z<Yz=Y
44 39 43 mt3d AtopGenran.𝑡AConnXAYAzXYAz<Y
45 20 ltpnfd AtopGenran.𝑡AConnXAYAzXYAY<+∞
46 pnfxr +∞*
47 elioo2 z*+∞*Yz+∞Yz<YY<+∞
48 31 46 47 sylancl AtopGenran.𝑡AConnXAYAzXYAYz+∞Yz<YY<+∞
49 20 44 45 48 mpbir3and AtopGenran.𝑡AConnXAYAzXYAYz+∞
50 inelcm Yz+∞YAz+∞A
51 49 19 50 syl2anc AtopGenran.𝑡AConnXAYAzXYAz+∞A
52 inss1 −∞zz+∞A−∞zz+∞
53 31 30 jctil AtopGenran.𝑡AConnXAYAzXYA−∞*z*
54 31 46 jctir AtopGenran.𝑡AConnXAYAzXYAz*+∞*
55 25 leidd AtopGenran.𝑡AConnXAYAzXYAzz
56 ioodisj −∞*z*z*+∞*zz−∞zz+∞=
57 53 54 55 56 syl21anc AtopGenran.𝑡AConnXAYAzXYA−∞zz+∞=
58 sseq0 −∞zz+∞A−∞zz+∞−∞zz+∞=−∞zz+∞A=
59 52 57 58 sylancr AtopGenran.𝑡AConnXAYAzXYA−∞zz+∞A=
60 30 a1i AtopGenran.𝑡AConnXAYAzXYA−∞*
61 46 a1i AtopGenran.𝑡AConnXAYAzXYA+∞*
62 25 mnfltd AtopGenran.𝑡AConnXAYAzXYA−∞<z
63 25 ltpnfd AtopGenran.𝑡AConnXAYAzXYAz<+∞
64 ioojoin −∞*z*+∞*−∞<zz<+∞−∞zzz+∞=−∞+∞
65 60 31 61 62 63 64 syl32anc AtopGenran.𝑡AConnXAYAzXYA−∞zzz+∞=−∞+∞
66 unass −∞zzz+∞=−∞zzz+∞
67 un12 −∞zzz+∞=z−∞zz+∞
68 66 67 eqtri −∞zzz+∞=z−∞zz+∞
69 ioomax −∞+∞=
70 65 68 69 3eqtr3g AtopGenran.𝑡AConnXAYAzXYAz−∞zz+∞=
71 4 70 sseqtrrd AtopGenran.𝑡AConnXAYAzXYAAz−∞zz+∞
72 disjsn Az=¬zA
73 13 72 sylibr AtopGenran.𝑡AConnXAYAzXYAAz=
74 disjssun Az=Az−∞zz+∞A−∞zz+∞
75 73 74 syl AtopGenran.𝑡AConnXAYAzXYAAz−∞zz+∞A−∞zz+∞
76 71 75 mpbid AtopGenran.𝑡AConnXAYAzXYAA−∞zz+∞
77 3 4 6 8 36 51 59 76 nconnsubb AtopGenran.𝑡AConnXAYAzXYA¬topGenran.𝑡AConn
78 77 ex AtopGenran.𝑡AConnXAYAzXYA¬topGenran.𝑡AConn
79 1 78 mt2d AtopGenran.𝑡AConnXAYA¬zXYA
80 79 eq0rdv AtopGenran.𝑡AConnXAYAXYA=
81 ssdif0 XYAXYA=
82 80 81 sylibr AtopGenran.𝑡AConnXAYAXYA