Definition df-phtpc

Description: Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of Hatcher p. 25. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Jun-2014)

	Ref	Expression
Assertion	df-phtpc	|- ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphtpc	|- ~=ph
1		vx	|- x
2		ctop	|- Top
3		vf	|- f
4		vg	|- g
5	3	cv	|- f
6	4	cv	|- g
7	5 6	cpr	|- { f , g }
8		cii	|- II
9		ccn	|- Cn
10	1	cv	|- x
11	8 10 9	co	|- ( II Cn x )
12	7 11	wss	|- { f , g } C_ ( II Cn x )
13		cphtpy	|- PHtpy
14	10 13	cfv	|- ( PHtpy ` x )
15	5 6 14	co	|- ( f ( PHtpy ` x ) g )
16		c0	|- (/)
17	15 16	wne	|- ( f ( PHtpy ` x ) g ) =/= (/)
18	12 17	wa	|- ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) )
19	18 3 4	copab	|- { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) }
20	1 2 19	cmpt	|- ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )
21	0 20	wceq	|- ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )