Metamath Proof Explorer

Theorem iccllysconn

Description: A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion iccllysconn 
|- ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Locally SConn )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> x e. ( topGen ` ran (,) ) )
2 inss1 
 |-  ( x i^i ( A [,] B ) ) C_ x
3 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> y e. ( x i^i ( A [,] B ) ) )
4 2 3 sselid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> y e. x )
5 tg2 
 |-  ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) -> E. z e. ran (,) ( y e. z /\ z C_ x ) )
6 1 4 5 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> E. z e. ran (,) ( y e. z /\ z C_ x ) )
7 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
8 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
9 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) ) )
10 7 8 9 mp2b 
 |-  ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) )
11 inss1 
 |-  ( z i^i ( A [,] B ) ) C_ z
12 simprrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> z C_ x )
13 11 12 sstrid 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( z i^i ( A [,] B ) ) C_ x )
14 simprrl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> y e. z )
15 simprl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> z = ( a (,) b ) )
16 15 ineq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( z i^i ( A [,] B ) ) = ( ( a (,) b ) i^i ( A [,] B ) ) )
17 16 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) = ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) )
18 ioosconn 
 |-  ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. SConn
19 ioossre 
 |-  ( a (,) b ) C_ RR
20 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) = ( ( topGen ` ran (,) ) |`t ( a (,) b ) )
21 20 resconn 
 |-  ( ( a (,) b ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. SConn <-> ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. Conn ) )
22 reconn 
 |-  ( ( a (,) b ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. Conn <-> A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) ) )
23 21 22 bitrd 
 |-  ( ( a (,) b ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. SConn <-> A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) ) )
24 19 23 ax-mp 
 |-  ( ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. SConn <-> A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) )
25 18 24 mpbi 
 |-  A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b )
26 inss1 
 |-  ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( a (,) b )
27 ssralv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( a (,) b ) -> ( A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) -> A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) ) )
28 27 ralimdv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( a (,) b ) -> ( A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) -> A. u e. ( a (,) b ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) ) )
29 ssralv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( a (,) b ) -> ( A. u e. ( a (,) b ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) ) )
30 28 29 syld 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( a (,) b ) -> ( A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) ) )
31 26 30 ax-mp 
 |-  ( A. u e. ( a (,) b ) A. v e. ( a (,) b ) ( u [,] v ) C_ ( a (,) b ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) )
32 25 31 mp1i 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) )
33 inss2 
 |-  ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( A [,] B )
34 iccconn 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )
35 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
36 reconn 
 |-  ( ( A [,] B ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn <-> A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) ) )
37 35 36 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn <-> A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) ) )
38 34 37 mpbid 
 |-  ( ( A e. RR /\ B e. RR ) -> A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) )
39 38 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) )
40 ssralv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( A [,] B ) -> ( A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) -> A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
41 40 ralimdv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( A [,] B ) -> ( A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) -> A. u e. ( A [,] B ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
42 ssralv 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( A [,] B ) -> ( A. u e. ( A [,] B ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
43 41 42 syld 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ ( A [,] B ) -> ( A. u e. ( A [,] B ) A. v e. ( A [,] B ) ( u [,] v ) C_ ( A [,] B ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
44 33 39 43 mpsyl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) )
45 ssin 
 |-  ( ( ( u [,] v ) C_ ( a (,) b ) /\ ( u [,] v ) C_ ( A [,] B ) ) <-> ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) )
46 45 2ralbii 
 |-  ( A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( ( u [,] v ) C_ ( a (,) b ) /\ ( u [,] v ) C_ ( A [,] B ) ) <-> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) )
47 r19.26-2 
 |-  ( A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( ( u [,] v ) C_ ( a (,) b ) /\ ( u [,] v ) C_ ( A [,] B ) ) <-> ( A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) /\ A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
48 46 47 bitr3i 
 |-  ( A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) <-> ( A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( a (,) b ) /\ A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( A [,] B ) ) )
49 32 44 48 sylanbrc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) )
50 26 19 sstri 
 |-  ( ( a (,) b ) i^i ( A [,] B ) ) C_ RR
51 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) = ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) )
52 51 resconn 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. SConn <-> ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. Conn ) )
53 reconn 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. Conn <-> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) ) )
54 52 53 bitrd 
 |-  ( ( ( a (,) b ) i^i ( A [,] B ) ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. SConn <-> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) ) )
55 50 54 ax-mp 
 |-  ( ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. SConn <-> A. u e. ( ( a (,) b ) i^i ( A [,] B ) ) A. v e. ( ( a (,) b ) i^i ( A [,] B ) ) ( u [,] v ) C_ ( ( a (,) b ) i^i ( A [,] B ) ) )
56 49 55 sylibr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( ( topGen ` ran (,) ) |`t ( ( a (,) b ) i^i ( A [,] B ) ) ) e. SConn )
57 17 56 eqeltrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn )
58 13 14 57 3jca 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) /\ ( z = ( a (,) b ) /\ ( y e. z /\ z C_ x ) ) ) -> ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) )
59 58 exp32 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( z = ( a (,) b ) -> ( ( y e. z /\ z C_ x ) -> ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) ) )
60 59 rexlimdvw 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( E. b e. RR* z = ( a (,) b ) -> ( ( y e. z /\ z C_ x ) -> ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) ) )
61 60 rexlimdvw 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( E. a e. RR* E. b e. RR* z = ( a (,) b ) -> ( ( y e. z /\ z C_ x ) -> ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) ) )
62 10 61 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( z e. ran (,) -> ( ( y e. z /\ z C_ x ) -> ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) ) )
63 62 reximdvai 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( E. z e. ran (,) ( y e. z /\ z C_ x ) -> E. z e. ran (,) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) )
64 retopbas 
 |-  ran (,) e. TopBases
65 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
66 ssrexv 
 |-  ( ran (,) C_ ( topGen ` ran (,) ) -> ( E. z e. ran (,) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) -> E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) )
67 64 65 66 mp2b 
 |-  ( E. z e. ran (,) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) -> E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) )
68 63 67 syl6 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> ( E. z e. ran (,) ( y e. z /\ z C_ x ) -> E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) )
69 6 68 mpd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( x e. ( topGen ` ran (,) ) /\ y e. ( x i^i ( A [,] B ) ) ) ) -> E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) )
70 69 ralrimivva 
 |-  ( ( A e. RR /\ B e. RR ) -> A. x e. ( topGen ` ran (,) ) A. y e. ( x i^i ( A [,] B ) ) E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) )
71 retop 
 |-  ( topGen ` ran (,) ) e. Top
72 ovex 
 |-  ( A [,] B ) e. _V
73 subislly 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Locally SConn <-> A. x e. ( topGen ` ran (,) ) A. y e. ( x i^i ( A [,] B ) ) E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) ) )
74 71 72 73 mp2an 
 |-  ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Locally SConn <-> A. x e. ( topGen ` ran (,) ) A. y e. ( x i^i ( A [,] B ) ) E. z e. ( topGen ` ran (,) ) ( ( z i^i ( A [,] B ) ) C_ x /\ y e. z /\ ( ( topGen ` ran (,) ) |`t ( z i^i ( A [,] B ) ) ) e. SConn ) )
75 70 74 sylibr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Locally SConn )