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

Definition df-pi1 18433
Description: Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-pi1  |-  pi 1  =  ( j  e. 
Top ,  y  e.  U. j  |->  ( ( j 
Om 1  y ) 
/.s  (  ~=ph  `  j ) ) )
Distinct variable group:    y, j

Detailed syntax breakdown of Definition df-pi1
StepHypRef Expression
1 cpi1 18428 . 2  class  pi 1
2 vj . . 3  set  j
3 vy . . 3  set  y
4 ctop 16558 . . 3  class  Top
52cv 1618 . . . 4  class  j
65cuni 3768 . . 3  class  U. j
73cv 1618 . . . . 5  class  y
8 comi 18426 . . . . 5  class  Om 1
95, 7, 8co 5757 . . . 4  class  ( j 
Om 1  y )
10 cphtpc 18394 . . . . 5  class  ~=ph
115, 10cfv 4638 . . . 4  class  (  ~=ph  `  j )
12 cqus 13335 . . . 4  class  /.s
139, 11, 12co 5757 . . 3  class  ( ( j  Om 1  y )  /.s  (  ~=ph  `  j ) )
142, 3, 4, 6, 13cmpt2 5759 . 2  class  ( j  e.  Top ,  y  e.  U. j  |->  ( ( j  Om 1 
y )  /.s  (  ~=ph  `  j ) ) )
151, 14wceq 1619 1  wff  pi 1  =  ( j  e. 
Top ,  y  e.  U. j  |->  ( ( j 
Om 1  y ) 
/.s  (  ~=ph  `  j ) ) )
Colors of variables: wff set class
This definition is referenced by:  pi1val  18462
  Copyright terms: Public domain W3C validator