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

Definition df-pi1 20580
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  |-  pi1 
=  ( j  e. 
Top ,  y  e.  U. j  |->  ( ( j 
Om1  y ) 
/.s  (  ~=ph  `  j ) ) )
Distinct variable group:    y, j

Detailed syntax breakdown of Definition df-pi1
StepHypRef Expression
1 cpi1 20575 . 2  class  pi1
2 vj . . 3  setvar  j
3 vy . . 3  setvar  y
4 ctop 18498 . . 3  class  Top
52cv 1368 . . . 4  class  j
65cuni 4091 . . 3  class  U. j
73cv 1368 . . . . 5  class  y
8 comi 20573 . . . . 5  class  Om1
95, 7, 8co 6091 . . . 4  class  ( j 
Om1  y )
10 cphtpc 20541 . . . . 5  class  ~=ph
115, 10cfv 5418 . . . 4  class  (  ~=ph  `  j )
12 cqus 14443 . . . 4  class  /.s
139, 11, 12co 6091 . . 3  class  ( ( j  Om1  y )  /.s  (  ~=ph  `  j ) )
142, 3, 4, 6, 13cmpt2 6093 . 2  class  ( j  e.  Top ,  y  e.  U. j  |->  ( ( j  Om1 
y )  /.s  (  ~=ph  `  j ) ) )
151, 14wceq 1369 1  wff  pi1 
=  ( j  e. 
Top ,  y  e.  U. j  |->  ( ( j 
Om1  y ) 
/.s  (  ~=ph  `  j ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  pi1val  20609
  Copyright terms: Public domain W3C validator