Definition df-pin

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)

	Ref	Expression
Assertion	df-pin	|- piN = ( j e. Top , p e. U. j |-> ( n e. NN0 |-> ( ( 1st ` ( ( j OmN p ) ` n ) ) /s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpin	|- piN
1		vj	|- j
2		ctop	|- Top
3		vp	|- p
4	1	cv	|- j
5	4	cuni	|- U. j
6		vn	|- n
7		cn0	|- NN0
8		c1st	|- 1st
9		comn	|- OmN
10	3	cv	|- p
11	4 10 9	co	|- ( j OmN p )
12	6	cv	|- n
13	12 11	cfv	|- ( ( j OmN p ) ` n )
14	13 8	cfv	|- ( 1st ` ( ( j OmN p ) ` n ) )
15		cqus	|- /s
16		cc0	|- 0
17	12 16	wceq	|- n = 0
18		vx	|- x
19		vy	|- y
20		vf	|- f
21		cii	|- II
22		ccn	|- Cn
23	21 4 22	co	|- ( II Cn j )
24	20	cv	|- f
25	16 24	cfv	|- ( f ` 0 )
26	18	cv	|- x
27	25 26	wceq	|- ( f ` 0 ) = x
28		c1	|- 1
29	28 24	cfv	|- ( f ` 1 )
30	19	cv	|- y
31	29 30	wceq	|- ( f ` 1 ) = y
32	27 31	wa	|- ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
33	32 20 23	wrex	|- E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
34	33 18 19	copab	|- { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) }
35		cphtpc	|- ~=ph
36		ctopn	|- TopOpen
37		cmin	|- -
38	12 28 37	co	|- ( n - 1 )
39	38 11	cfv	|- ( ( j OmN p ) ` ( n - 1 ) )
40	39 8	cfv	|- ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) )
41	40 36	cfv	|- ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) )
42	41 35	cfv	|- ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) )
43	17 34 42	cif	|- if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) )
44	14 43 15	co	|- ( ( 1st ` ( ( j OmN p ) ` n ) ) /s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) )
45	6 7 44	cmpt	|- ( n e. NN0 |-> ( ( 1st ` ( ( j OmN p ) ` n ) ) /s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) ) )
46	1 3 2 5 45	cmpo	|- ( j e. Top , p e. U. j |-> ( n e. NN0 |-> ( ( 1st ` ( ( j OmN p ) ` n ) ) /s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) ) ) )
47	0 46	wceq	|- piN = ( j e. Top , p e. U. j |-> ( n e. NN0 |-> ( ( 1st ` ( ( j OmN p ) ` n ) ) /s if ( n = 0 , { <. x , y >. | E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) } , ( ~=ph ` ( TopOpen ` ( 1st ` ( ( j OmN p ) ` ( n - 1 ) ) ) ) ) ) ) ) )