Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pcon Structured version   Unicode version

Definition df-pcon 27115
Description: Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the unit interval) that goes from  x to  y for any points  x ,  y in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-pcon  |- PCon  =  {
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 ) }
Distinct variable group:    f, j, x, y

Detailed syntax breakdown of Definition df-pcon
StepHypRef Expression
1 cpcon 27113 . 2  class PCon
2 cc0 9287 . . . . . . . . 9  class  0
3 vf . . . . . . . . . 10  setvar  f
43cv 1368 . . . . . . . . 9  class  f
52, 4cfv 5423 . . . . . . . 8  class  ( f `
 0 )
6 vx . . . . . . . . 9  setvar  x
76cv 1368 . . . . . . . 8  class  x
85, 7wceq 1369 . . . . . . 7  wff  ( f `
 0 )  =  x
9 c1 9288 . . . . . . . . 9  class  1
109, 4cfv 5423 . . . . . . . 8  class  ( f `
 1 )
11 vy . . . . . . . . 9  setvar  y
1211cv 1368 . . . . . . . 8  class  y
1310, 12wceq 1369 . . . . . . 7  wff  ( f `
 1 )  =  y
148, 13wa 369 . . . . . 6  wff  ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y )
15 cii 20456 . . . . . . 7  class  II
16 vj . . . . . . . 8  setvar  j
1716cv 1368 . . . . . . 7  class  j
18 ccn 18833 . . . . . . 7  class  Cn
1915, 17, 18co 6096 . . . . . 6  class  ( II 
Cn  j )
2014, 3, 19wrex 2721 . . . . 5  wff  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2117cuni 4096 . . . . 5  class  U. j
2220, 11, 21wral 2720 . . . 4  wff  A. y  e.  U. j E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2322, 6, 21wral 2720 . . 3  wff  A. x  e.  U. j A. y  e.  U. j E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
24 ctop 18503 . . 3  class  Top
2523, 16, 24crab 2724 . 2  class  { 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 ) }
261, 25wceq 1369 1  wff PCon  =  {
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 ) }
Colors of variables: wff setvar class
This definition is referenced by:  ispcon  27117
  Copyright terms: Public domain W3C validator