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

Definition df-pcon 24865
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 24863 . 2  class PCon
2 cc0 8950 . . . . . . . . 9  class  0
3 vf . . . . . . . . . 10  set  f
43cv 1648 . . . . . . . . 9  class  f
52, 4cfv 5417 . . . . . . . 8  class  ( f `
 0 )
6 vx . . . . . . . . 9  set  x
76cv 1648 . . . . . . . 8  class  x
85, 7wceq 1649 . . . . . . 7  wff  ( f `
 0 )  =  x
9 c1 8951 . . . . . . . . 9  class  1
109, 4cfv 5417 . . . . . . . 8  class  ( f `
 1 )
11 vy . . . . . . . . 9  set  y
1211cv 1648 . . . . . . . 8  class  y
1310, 12wceq 1649 . . . . . . 7  wff  ( f `
 1 )  =  y
148, 13wa 359 . . . . . 6  wff  ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y )
15 cii 18862 . . . . . . 7  class  II
16 vj . . . . . . . 8  set  j
1716cv 1648 . . . . . . 7  class  j
18 ccn 17246 . . . . . . 7  class  Cn
1915, 17, 18co 6044 . . . . . 6  class  ( II 
Cn  j )
2014, 3, 19wrex 2671 . . . . 5  wff  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2117cuni 3979 . . . . 5  class  U. j
2220, 11, 21wral 2670 . . . 4  wff  A. y  e.  U. j E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
2322, 6, 21wral 2670 . . 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 16917 . . 3  class  Top
2523, 16, 24crab 2674 . 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 1649 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  24867
  Copyright terms: Public domain W3C validator