Metamath Proof Explorer

Theorem pconnconn

Description: A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion pconnconn 
|- ( J e. PConn -> J e. Conn )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) <-> ( ( x =/= (/) /\ y =/= (/) ) /\ ( x i^i y ) = (/) ) )
2 n0 
 |-  ( x =/= (/) <-> E. a a e. x )
3 n0 
 |-  ( y =/= (/) <-> E. b b e. y )
4 2 3 anbi12i 
 |-  ( ( x =/= (/) /\ y =/= (/) ) <-> ( E. a a e. x /\ E. b b e. y ) )
5 exdistrv 
 |-  ( E. a E. b ( a e. x /\ b e. y ) <-> ( E. a a e. x /\ E. b b e. y ) )
6 4 5 bitr4i 
 |-  ( ( x =/= (/) /\ y =/= (/) ) <-> E. a E. b ( a e. x /\ b e. y ) )
7 simpll 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> J e. PConn )
8 simprll 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> a e. x )
9 simplrl 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> x e. J )
10 elunii 
 |-  ( ( a e. x /\ x e. J ) -> a e. U. J )
11 8 9 10 syl2anc 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> a e. U. J )
12 simprlr 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> b e. y )
13 simplrr 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> y e. J )
14 elunii 
 |-  ( ( b e. y /\ y e. J ) -> b e. U. J )
15 12 13 14 syl2anc 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> b e. U. J )
16 eqid 
 |-  U. J = U. J
17 16 pconncn 
 |-  ( ( J e. PConn /\ a e. U. J /\ b e. U. J ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) )
18 7 11 15 17 syl3anc 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) )
19 simplrr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( x i^i y ) = (/) )
20 simplrr 
 |-  ( ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) -> ( f ` 1 ) = b )
21 20 adantl 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( f ` 1 ) = b )
22 iiuni 
 |-  ( 0 [,] 1 ) = U. II
23 iiconn 
 |-  II e. Conn
24 23 a1i 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> II e. Conn )
25 simprll 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> f e. ( II Cn J ) )
26 9 adantr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> x e. J )
27 uncom 
 |-  ( y u. x ) = ( x u. y )
28 simprr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( x u. y ) = U. J )
29 27 28 syl5eq 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( y u. x ) = U. J )
30 13 adantr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> y e. J )
31 elssuni 
 |-  ( y e. J -> y C_ U. J )
32 30 31 syl 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> y C_ U. J )
33 incom 
 |-  ( y i^i x ) = ( x i^i y )
34 33 19 syl5eq 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( y i^i x ) = (/) )
35 uneqdifeq 
 |-  ( ( y C_ U. J /\ ( y i^i x ) = (/) ) -> ( ( y u. x ) = U. J <-> ( U. J \ y ) = x ) )
36 32 34 35 syl2anc 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( ( y u. x ) = U. J <-> ( U. J \ y ) = x ) )
37 29 36 mpbid 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( U. J \ y ) = x )
38 pconntop 
 |-  ( J e. PConn -> J e. Top )
39 38 ad3antrrr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> J e. Top )
40 16 opncld 
 |-  ( ( J e. Top /\ y e. J ) -> ( U. J \ y ) e. ( Clsd ` J ) )
41 39 30 40 syl2anc 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( U. J \ y ) e. ( Clsd ` J ) )
42 37 41 eqeltrrd 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> x e. ( Clsd ` J ) )
43 0elunit 
 |-  0 e. ( 0 [,] 1 )
44 43 a1i 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> 0 e. ( 0 [,] 1 ) )
45 simplrl 
 |-  ( ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) -> ( f ` 0 ) = a )
46 45 adantl 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( f ` 0 ) = a )
47 8 adantr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> a e. x )
48 46 47 eqeltrd 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( f ` 0 ) e. x )
49 22 24 25 26 42 44 48 conncn 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> f : ( 0 [,] 1 ) --> x )
50 1elunit 
 |-  1 e. ( 0 [,] 1 )
51 ffvelrn 
 |-  ( ( f : ( 0 [,] 1 ) --> x /\ 1 e. ( 0 [,] 1 ) ) -> ( f ` 1 ) e. x )
52 49 50 51 sylancl 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( f ` 1 ) e. x )
53 21 52 eqeltrrd 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> b e. x )
54 12 adantr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> b e. y )
55 inelcm 
 |-  ( ( b e. x /\ b e. y ) -> ( x i^i y ) =/= (/) )
56 53 54 55 syl2anc 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> ( x i^i y ) =/= (/) )
57 19 56 pm2.21ddne 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) /\ ( x u. y ) = U. J ) ) -> -. ( x u. y ) = U. J )
58 57 expr 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) ) -> ( ( x u. y ) = U. J -> -. ( x u. y ) = U. J ) )
59 58 pm2.01d 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) ) -> -. ( x u. y ) = U. J )
60 59 neqned 
 |-  ( ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = a /\ ( f ` 1 ) = b ) ) ) -> ( x u. y ) =/= U. J )
61 18 60 rexlimddv 
 |-  ( ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) /\ ( ( a e. x /\ b e. y ) /\ ( x i^i y ) = (/) ) ) -> ( x u. y ) =/= U. J )
62 61 exp32 
 |-  ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) -> ( ( a e. x /\ b e. y ) -> ( ( x i^i y ) = (/) -> ( x u. y ) =/= U. J ) ) )
63 62 exlimdvv 
 |-  ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) -> ( E. a E. b ( a e. x /\ b e. y ) -> ( ( x i^i y ) = (/) -> ( x u. y ) =/= U. J ) ) )
64 6 63 syl5bi 
 |-  ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) -> ( ( x =/= (/) /\ y =/= (/) ) -> ( ( x i^i y ) = (/) -> ( x u. y ) =/= U. J ) ) )
65 64 impd 
 |-  ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) -> ( ( ( x =/= (/) /\ y =/= (/) ) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) )
66 1 65 syl5bi 
 |-  ( ( J e. PConn /\ ( x e. J /\ y e. J ) ) -> ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) )
67 66 ralrimivva 
 |-  ( J e. PConn -> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) )
68 16 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
69 38 68 sylib 
 |-  ( J e. PConn -> J e. ( TopOn ` U. J ) )
70 dfconn2 
 |-  ( J e. ( TopOn ` U. J ) -> ( J e. Conn <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
71 69 70 syl 
 |-  ( J e. PConn -> ( J e. Conn <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
72 67 71 mpbird 
 |-  ( J e. PConn -> J e. Conn )