MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pin Unicode version

Definition df-pin 18507
Description: Define the n-th homotopy group, which is formed by taking the 
n-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the  n-th loop space, which is the  n  -  1-th loop space. For  n  =  0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the  0-th homotopy group is the set of path components of  X. (Since the  0-th loop space does not have a group operation, neither does the  0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-pin  |-  pi N  =  ( j  e. 
Top ,  p  e.  U. j  |->  ( n  e. 
NN0  |->  ( ( 1st `  ( ( j  Om N  p ) `  n
) )  /.s  if (
n  =  0 ,  { <. x ,  y
>.  |  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y ) } , 
(  ~=ph  `  ( TopOpen `  ( 1st `  ( ( j 
Om N  p ) `
 ( n  - 
1 ) ) ) ) ) ) ) ) )
Distinct variable group:    f, j, n, p, x, y

Detailed syntax breakdown of Definition df-pin
StepHypRef Expression
1 cpin 18502 . 2  class  pi N
2 vj . . 3  set  j
3 vp . . 3  set  p
4 ctop 16631 . . 3  class  Top
52cv 1622 . . . 4  class  j
65cuni 3827 . . 3  class  U. j
7 vn . . . 4  set  n
8 cn0 9965 . . . 4  class  NN0
97cv 1622 . . . . . . 7  class  n
103cv 1622 . . . . . . . 8  class  p
11 comn 18500 . . . . . . . 8  class  Om N
125, 10, 11co 5858 . . . . . . 7  class  ( j 
Om N  p )
139, 12cfv 5255 . . . . . 6  class  ( ( j  Om N  p ) `  n )
14 c1st 6120 . . . . . 6  class  1st
1513, 14cfv 5255 . . . . 5  class  ( 1st `  ( ( j  Om N  p ) `  n
) )
16 cc0 8737 . . . . . . 7  class  0
179, 16wceq 1623 . . . . . 6  wff  n  =  0
18 vf . . . . . . . . . . . 12  set  f
1918cv 1622 . . . . . . . . . . 11  class  f
2016, 19cfv 5255 . . . . . . . . . 10  class  ( f `
 0 )
21 vx . . . . . . . . . . 11  set  x
2221cv 1622 . . . . . . . . . 10  class  x
2320, 22wceq 1623 . . . . . . . . 9  wff  ( f `
 0 )  =  x
24 c1 8738 . . . . . . . . . . 11  class  1
2524, 19cfv 5255 . . . . . . . . . 10  class  ( f `
 1 )
26 vy . . . . . . . . . . 11  set  y
2726cv 1622 . . . . . . . . . 10  class  y
2825, 27wceq 1623 . . . . . . . . 9  wff  ( f `
 1 )  =  y
2923, 28wa 358 . . . . . . . 8  wff  ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y )
30 cii 18379 . . . . . . . . 9  class  II
31 ccn 16954 . . . . . . . . 9  class  Cn
3230, 5, 31co 5858 . . . . . . . 8  class  ( II 
Cn  j )
3329, 18, 32wrex 2544 . . . . . . 7  wff  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y )
3433, 21, 26copab 4076 . . . . . 6  class  { <. x ,  y >.  |  E. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y ) }
35 cmin 9037 . . . . . . . . . . 11  class  -
369, 24, 35co 5858 . . . . . . . . . 10  class  ( n  -  1 )
3736, 12cfv 5255 . . . . . . . . 9  class  ( ( j  Om N  p ) `  ( n  -  1 ) )
3837, 14cfv 5255 . . . . . . . 8  class  ( 1st `  ( ( j  Om N  p ) `  (
n  -  1 ) ) )
39 ctopn 13326 . . . . . . . 8  class  TopOpen
4038, 39cfv 5255 . . . . . . 7  class  ( TopOpen `  ( 1st `  ( ( j  Om N  p ) `  ( n  -  1 ) ) ) )
41 cphtpc 18467 . . . . . . 7  class  ~=ph
4240, 41cfv 5255 . . . . . 6  class  (  ~=ph  `  ( TopOpen `  ( 1st `  ( ( j  Om N  p ) `  (
n  -  1 ) ) ) ) )
4317, 34, 42cif 3565 . . . . 5  class  if ( n  =  0 ,  { <. x ,  y
>.  |  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y ) } , 
(  ~=ph  `  ( TopOpen `  ( 1st `  ( ( j 
Om N  p ) `
 ( n  - 
1 ) ) ) ) ) )
44 cqus 13408 . . . . 5  class  /.s
4515, 43, 44co 5858 . . . 4  class  ( ( 1st `  ( ( j  Om N  p ) `  n ) )  /.s  if ( n  =  0 ,  { <. x ,  y >.  |  E. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y ) } ,  (  ~=ph  `  ( TopOpen
`  ( 1st `  (
( j  Om N  p ) `  (
n  -  1 ) ) ) ) ) ) )
467, 8, 45cmpt 4077 . . 3  class  ( n  e.  NN0  |->  ( ( 1st `  ( ( j  Om N  p ) `  n ) )  /.s  if ( n  =  0 ,  { <. x ,  y >.  |  E. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y ) } ,  (  ~=ph  `  ( TopOpen
`  ( 1st `  (
( j  Om N  p ) `  (
n  -  1 ) ) ) ) ) ) ) )
472, 3, 4, 6, 46cmpt2 5860 . 2  class  ( j  e.  Top ,  p  e.  U. j  |->  ( n  e.  NN0  |->  ( ( 1st `  ( ( j  Om N  p ) `  n ) )  /.s  if ( n  =  0 ,  { <. x ,  y >.  |  E. f  e.  ( II  Cn  j ) ( ( f `  0 )  =  x  /\  (
f `  1 )  =  y ) } ,  (  ~=ph  `  ( TopOpen
`  ( 1st `  (
( j  Om N  p ) `  (
n  -  1 ) ) ) ) ) ) ) ) )
481, 47wceq 1623 1  wff  pi N  =  ( j  e. 
Top ,  p  e.  U. j  |->  ( n  e. 
NN0  |->  ( ( 1st `  ( ( j  Om N  p ) `  n
) )  /.s  if (
n  =  0 ,  { <. x ,  y
>.  |  E. f  e.  ( II  Cn  j
) ( ( f `
 0 )  =  x  /\  ( f `
 1 )  =  y ) } , 
(  ~=ph  `  ( TopOpen `  ( 1st `  ( ( j 
Om N  p ) `
 ( n  - 
1 ) ) ) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator