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

Definition df-pcon 23752
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 23750 . 2  class PCon
2 cc0 8737 . . . . . . . . 9  class  0
3 vf . . . . . . . . . 10  set  f
43cv 1622 . . . . . . . . 9  class  f
52, 4cfv 5255 . . . . . . . 8  class  ( f `
 0 )
6 vx . . . . . . . . 9  set  x
76cv 1622 . . . . . . . 8  class  x
85, 7wceq 1623 . . . . . . 7  wff  ( f `
 0 )  =  x
9 c1 8738 . . . . . . . . 9  class  1
109, 4cfv 5255 . . . . . . . 8  class  ( f `
 1 )
11 vy . . . . . . . . 9  set  y
1211cv 1622 . . . . . . . 8  class  y
1310, 12wceq 1623 . . . . . . 7  wff  ( f `
 1 )  =  y
148, 13wa 358 . . . . . 6  wff  ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y )
15 cii 18379 . . . . . . 7  class  II
16 vj . . . . . . . 8  set  j
1716cv 1622 . . . . . . 7  class  j
18 ccn 16954 . . . . . . 7  class  Cn
1915, 17, 18co 5858 . . . . . 6  class  ( II 
Cn  j )
2014, 3, 19wrex 2544 . . . . 5  wff  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2117cuni 3827 . . . . 5  class  U. j
2220, 11, 21wral 2543 . . . 4  wff  A. y  e.  U. j E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2322, 6, 21wral 2543 . . 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 16631 . . 3  class  Top
2523, 16, 24crab 2547 . 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 1623 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 set class
This definition is referenced by:  ispcon  23754
  Copyright terms: Public domain W3C validator