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