Metamath Proof Explorer

Theorem connpconn

Description: A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015)

Ref Expression
Assertion connpconn 
|- ( ( J e. Conn /\ J e. N-Locally PConn ) -> J e. PConn )

Proof

Step Hyp Ref Expression
1 conntop 
 |-  ( J e. Conn -> J e. Top )
2 1 adantr 
 |-  ( ( J e. Conn /\ J e. N-Locally PConn ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 simpll 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> J e. Conn )
5 inss1 
 |-  ( J i^i ( Clsd ` J ) ) C_ J
6 simplr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> J e. N-Locally PConn )
7 1 ad2antrr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> J e. Top )
8 3 topopn 
 |-  ( J e. Top -> U. J e. J )
9 7 8 syl 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> U. J e. J )
10 simprr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> z e. U. J )
11 nlly2i 
 |-  ( ( J e. N-Locally PConn /\ U. J e. J /\ z e. U. J ) -> E. s e. ~P U. J E. u e. J ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) )
12 6 9 10 11 syl3anc 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> E. s e. ~P U. J E. u e. J ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) )
13 simprr1 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> z e. u )
14 eqeq2 
 |-  ( y = w -> ( ( f ` 1 ) = y <-> ( f ` 1 ) = w ) )
15 14 anbi2d 
 |-  ( y = w -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) ) )
16 15 rexbidv 
 |-  ( y = w -> ( E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) ) )
17 16 elrab 
 |-  ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } <-> ( w e. U. J /\ E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) ) )
18 17 simprbi 
 |-  ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) )
19 simprr3 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> ( J |`t s ) e. PConn )
20 19 adantr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> ( J |`t s ) e. PConn )
21 simprr2 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> u C_ s )
22 21 adantr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> u C_ s )
23 simprll 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> w e. u )
24 22 23 sseldd 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> w e. s )
25 7 ad2antrr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> J e. Top )
26 elpwi 
 |-  ( s e. ~P U. J -> s C_ U. J )
27 26 ad2antrl 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> s C_ U. J )
28 27 adantr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> s C_ U. J )
29 3 restuni 
 |-  ( ( J e. Top /\ s C_ U. J ) -> s = U. ( J |`t s ) )
30 25 28 29 syl2anc 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> s = U. ( J |`t s ) )
31 24 30 eleqtrd 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> w e. U. ( J |`t s ) )
32 simprr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> y e. u )
33 22 32 sseldd 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> y e. s )
34 33 30 eleqtrd 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> y e. U. ( J |`t s ) )
35 eqid 
 |-  U. ( J |`t s ) = U. ( J |`t s )
36 35 pconncn 
 |-  ( ( ( J |`t s ) e. PConn /\ w e. U. ( J |`t s ) /\ y e. U. ( J |`t s ) ) -> E. h e. ( II Cn ( J |`t s ) ) ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) )
37 20 31 34 36 syl3anc 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> E. h e. ( II Cn ( J |`t s ) ) ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) )
38 simplrl 
 |-  ( ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) -> g e. ( II Cn J ) )
39 38 ad2antlr 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> g e. ( II Cn J ) )
40 25 adantr 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> J e. Top )
41 cnrest2r 
 |-  ( J e. Top -> ( II Cn ( J |`t s ) ) C_ ( II Cn J ) )
42 40 41 syl 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( II Cn ( J |`t s ) ) C_ ( II Cn J ) )
43 simprl 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> h e. ( II Cn ( J |`t s ) ) )
44 42 43 sseldd 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> h e. ( II Cn J ) )
45 simplrr 
 |-  ( ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) -> ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) )
46 45 ad2antlr 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) )
47 46 simprd 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( g ` 1 ) = w )
48 simprrl 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( h ` 0 ) = w )
49 47 48 eqtr4d 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( g ` 1 ) = ( h ` 0 ) )
50 39 44 49 pcocn 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( g ( *p ` J ) h ) e. ( II Cn J ) )
51 39 44 pco0 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( ( g ( *p ` J ) h ) ` 0 ) = ( g ` 0 ) )
52 46 simpld 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( g ` 0 ) = x )
53 51 52 eqtrd 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( ( g ( *p ` J ) h ) ` 0 ) = x )
54 39 44 pco1 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( ( g ( *p ` J ) h ) ` 1 ) = ( h ` 1 ) )
55 simprrr 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( h ` 1 ) = y )
56 54 55 eqtrd 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> ( ( g ( *p ` J ) h ) ` 1 ) = y )
57 fveq1 
 |-  ( f = ( g ( *p ` J ) h ) -> ( f ` 0 ) = ( ( g ( *p ` J ) h ) ` 0 ) )
58 57 eqeq1d 
 |-  ( f = ( g ( *p ` J ) h ) -> ( ( f ` 0 ) = x <-> ( ( g ( *p ` J ) h ) ` 0 ) = x ) )
59 fveq1 
 |-  ( f = ( g ( *p ` J ) h ) -> ( f ` 1 ) = ( ( g ( *p ` J ) h ) ` 1 ) )
60 59 eqeq1d 
 |-  ( f = ( g ( *p ` J ) h ) -> ( ( f ` 1 ) = y <-> ( ( g ( *p ` J ) h ) ` 1 ) = y ) )
61 58 60 anbi12d 
 |-  ( f = ( g ( *p ` J ) h ) -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( ( g ( *p ` J ) h ) ` 0 ) = x /\ ( ( g ( *p ` J ) h ) ` 1 ) = y ) ) )
62 61 rspcev 
 |-  ( ( ( g ( *p ` J ) h ) e. ( II Cn J ) /\ ( ( ( g ( *p ` J ) h ) ` 0 ) = x /\ ( ( g ( *p ` J ) h ) ` 1 ) = y ) ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
63 50 53 56 62 syl12anc 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) /\ ( h e. ( II Cn ( J |`t s ) ) /\ ( ( h ` 0 ) = w /\ ( h ` 1 ) = y ) ) ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
64 37 63 rexlimddv 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) /\ y e. u ) ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
65 64 anassrs 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) ) /\ y e. u ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
66 65 ralrimiva 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ ( w e. u /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) ) -> A. y e. u E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
67 66 anassrs 
 |-  ( ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) ) -> A. y e. u E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
68 67 rexlimdvaa 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> ( E. g e. ( II Cn J ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) -> A. y e. u E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
69 21 adantr 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> u C_ s )
70 simplrl 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> s e. ~P U. J )
71 70 26 syl 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> s C_ U. J )
72 69 71 sstrd 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> u C_ U. J )
73 68 72 jctild 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> ( E. g e. ( II Cn J ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) -> ( u C_ U. J /\ A. y e. u E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) ) )
74 fveq1 
 |-  ( f = g -> ( f ` 0 ) = ( g ` 0 ) )
75 74 eqeq1d 
 |-  ( f = g -> ( ( f ` 0 ) = x <-> ( g ` 0 ) = x ) )
76 fveq1 
 |-  ( f = g -> ( f ` 1 ) = ( g ` 1 ) )
77 76 eqeq1d 
 |-  ( f = g -> ( ( f ` 1 ) = w <-> ( g ` 1 ) = w ) )
78 75 77 anbi12d 
 |-  ( f = g -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) <-> ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) ) )
79 78 cbvrexvw 
 |-  ( E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) <-> E. g e. ( II Cn J ) ( ( g ` 0 ) = x /\ ( g ` 1 ) = w ) )
80 ssrab 
 |-  ( u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } <-> ( u C_ U. J /\ A. y e. u E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
81 73 79 80 3imtr4g 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> ( E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = w ) -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) )
82 18 81 syl5 
 |-  ( ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) /\ w e. u ) -> ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) )
83 82 ralrimiva 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) )
84 13 83 jca 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ ( s e. ~P U. J /\ ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) ) ) -> ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) )
85 84 expr 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ s e. ~P U. J ) -> ( ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) -> ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) ) )
86 85 reximdv 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) /\ s e. ~P U. J ) -> ( E. u e. J ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) -> E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) ) )
87 86 rexlimdva 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> ( E. s e. ~P U. J E. u e. J ( z e. u /\ u C_ s /\ ( J |`t s ) e. PConn ) -> E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) ) )
88 12 87 mpd 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ ( x e. U. J /\ z e. U. J ) ) -> E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) )
89 88 anassrs 
 |-  ( ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) /\ z e. U. J ) -> E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) )
90 89 ralrimiva 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> A. z e. U. J E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) )
91 1 ad2antrr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> J e. Top )
92 ssrab2 
 |-  { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } C_ U. J
93 3 isclo2 
 |-  ( ( J e. Top /\ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } C_ U. J ) -> ( { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } e. ( J i^i ( Clsd ` J ) ) <-> A. z e. U. J E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) ) )
94 91 92 93 sylancl 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> ( { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } e. ( J i^i ( Clsd ` J ) ) <-> A. z e. U. J E. u e. J ( z e. u /\ A. w e. u ( w e. { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } -> u C_ { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } ) ) ) )
95 90 94 mpbird 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } e. ( J i^i ( Clsd ` J ) ) )
96 5 95 sseldi 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } e. J )
97 simpr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> x e. U. J )
98 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
99 98 a1i 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
100 3 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
101 91 100 sylib 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> J e. ( TopOn ` U. J ) )
102 cnconst2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` U. J ) /\ x e. U. J ) -> ( ( 0 [,] 1 ) X. { x } ) e. ( II Cn J ) )
103 99 101 97 102 syl3anc 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> ( ( 0 [,] 1 ) X. { x } ) e. ( II Cn J ) )
104 0elunit 
 |-  0 e. ( 0 [,] 1 )
105 vex 
 |-  x e. _V
106 105 fvconst2 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) = x )
107 104 106 mp1i 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) = x )
108 1elunit 
 |-  1 e. ( 0 [,] 1 )
109 105 fvconst2 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) = x )
110 108 109 mp1i 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) = x )
111 eqeq2 
 |-  ( y = x -> ( ( f ` 1 ) = y <-> ( f ` 1 ) = x ) )
112 111 anbi2d 
 |-  ( y = x -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = x /\ ( f ` 1 ) = x ) ) )
113 fveq1 
 |-  ( f = ( ( 0 [,] 1 ) X. { x } ) -> ( f ` 0 ) = ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) )
114 113 eqeq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { x } ) -> ( ( f ` 0 ) = x <-> ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) = x ) )
115 fveq1 
 |-  ( f = ( ( 0 [,] 1 ) X. { x } ) -> ( f ` 1 ) = ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) )
116 115 eqeq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { x } ) -> ( ( f ` 1 ) = x <-> ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) = x ) )
117 114 116 anbi12d 
 |-  ( f = ( ( 0 [,] 1 ) X. { x } ) -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = x ) <-> ( ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) = x /\ ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) = x ) ) )
118 112 117 rspc2ev 
 |-  ( ( x e. U. J /\ ( ( 0 [,] 1 ) X. { x } ) e. ( II Cn J ) /\ ( ( ( ( 0 [,] 1 ) X. { x } ) ` 0 ) = x /\ ( ( ( 0 [,] 1 ) X. { x } ) ` 1 ) = x ) ) -> E. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
119 97 103 107 110 118 syl112anc 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> E. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
120 rabn0 
 |-  ( { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } =/= (/) <-> E. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
121 119 120 sylibr 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } =/= (/) )
122 inss2 
 |-  ( J i^i ( Clsd ` J ) ) C_ ( Clsd ` J )
123 122 95 sseldi 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } e. ( Clsd ` J ) )
124 3 4 96 121 123 connclo 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } = U. J )
125 124 eqcomd 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> U. J = { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } )
126 rabid2 
 |-  ( U. J = { y e. U. J | E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } <-> A. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
127 125 126 sylib 
 |-  ( ( ( J e. Conn /\ J e. N-Locally PConn ) /\ x e. U. J ) -> A. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
128 127 ralrimiva 
 |-  ( ( J e. Conn /\ J e. N-Locally PConn ) -> A. x e. U. J A. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
129 3 ispconn 
 |-  ( J e. PConn <-> ( J e. Top /\ A. x e. U. J A. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
130 2 128 129 sylanbrc 
 |-  ( ( J e. Conn /\ J e. N-Locally PConn ) -> J e. PConn )