Definition df-pi1 22808

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

Step	Hyp	Ref	Expression
1		cpi1 22803	. 2 class pi1
2		vj	. . 3 setvar j
3		vy	. . 3 setvar y
4		ctop 20698	. . 3 class Top
5	2	cv 1482	. . . 4 class j
6	5	cuni 4436	. . 3 class U. j
7	3	cv 1482	. . . . 5 class y
8		comi 22801	. . . . 5 class Om1
9	5, 7, 8	co 6650	. . . 4 class ( j Om1 y )
10		cphtpc 22768	. . . . 5 class ~=ph
11	5, 10	cfv 5888	. . . 4 class ( ~=ph ` j )
12		cqus 16165	. . . 4 class /.s
13	9, 11, 12	co 6650	. . 3 class ( ( j Om1 y ) /.s ( ~=ph ` j ) )
14	2, 3, 4, 6, 13	cmpt2 6652	. 2 class ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /.s ( ~=ph ` j ) ) )
15	1, 14	wceq 1483	1 wff pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /.s ( ~=ph ` j ) ) )

This definition is referenced by:  pi1val  22837