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

Definition df-scon 23768
Description: Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.)
Assertion
Ref Expression
df-scon  |- SCon  =  {
j  e. PCon  |  A. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  ( f ` 
1 )  ->  f
(  ~=ph  `  j )
( ( 0 [,] 1 )  X.  {
( f `  0
) } ) ) }
Distinct variable group:    f, j

Detailed syntax breakdown of Definition df-scon
StepHypRef Expression
1 cscon 23766 . 2  class SCon
2 cc0 8753 . . . . . . 7  class  0
3 vf . . . . . . . 8  set  f
43cv 1631 . . . . . . 7  class  f
52, 4cfv 5271 . . . . . 6  class  ( f `
 0 )
6 c1 8754 . . . . . . 7  class  1
76, 4cfv 5271 . . . . . 6  class  ( f `
 1 )
85, 7wceq 1632 . . . . 5  wff  ( f `
 0 )  =  ( f `  1
)
9 cicc 10675 . . . . . . . 8  class  [,]
102, 6, 9co 5874 . . . . . . 7  class  ( 0 [,] 1 )
115csn 3653 . . . . . . 7  class  { ( f `  0 ) }
1210, 11cxp 4703 . . . . . 6  class  ( ( 0 [,] 1 )  X.  { ( f `
 0 ) } )
13 vj . . . . . . . 8  set  j
1413cv 1631 . . . . . . 7  class  j
15 cphtpc 18483 . . . . . . 7  class  ~=ph
1614, 15cfv 5271 . . . . . 6  class  (  ~=ph  `  j )
174, 12, 16wbr 4039 . . . . 5  wff  f ( 
~=ph  `  j ) ( ( 0 [,] 1
)  X.  { ( f `  0 ) } )
188, 17wi 4 . . . 4  wff  ( ( f `  0 )  =  ( f ` 
1 )  ->  f
(  ~=ph  `  j )
( ( 0 [,] 1 )  X.  {
( f `  0
) } ) )
19 cii 18395 . . . . 5  class  II
20 ccn 16970 . . . . 5  class  Cn
2119, 14, 20co 5874 . . . 4  class  ( II 
Cn  j )
2218, 3, 21wral 2556 . . 3  wff  A. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  ( f `  1
)  ->  f (  ~=ph  `  j ) ( ( 0 [,] 1 )  X.  { ( f `
 0 ) } ) )
23 cpcon 23765 . . 3  class PCon
2422, 13, 23crab 2560 . 2  class  { j  e. PCon  |  A. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  ( f `  1
)  ->  f (  ~=ph  `  j ) ( ( 0 [,] 1 )  X.  { ( f `
 0 ) } ) ) }
251, 24wceq 1632 1  wff SCon  =  {
j  e. PCon  |  A. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  ( f ` 
1 )  ->  f
(  ~=ph  `  j )
( ( 0 [,] 1 )  X.  {
( f `  0
) } ) ) }
Colors of variables: wff set class
This definition is referenced by:  isscon  23772
  Copyright terms: Public domain W3C validator