Definition df-phtpc 22791

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.)

Assertion

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

Distinct variable group:   x, f, g

Detailed syntax breakdown of Definition df-phtpc

Step	Hyp	Ref	Expression
1		cphtpc 22768	. 2 class ~=ph
2		vx	. . 3 setvar x
3		ctop 20698	. . 3 class Top
4		vf	. . . . . . . 8 setvar f
5	4	cv 1482	. . . . . . 7 class f
6		vg	. . . . . . . 8 setvar g
7	6	cv 1482	. . . . . . 7 class g
8	5, 7	cpr 4179	. . . . . 6 class { f , g }
9		cii 22678	. . . . . . 7 class II
10	2	cv 1482	. . . . . . 7 class x
11		ccn 21028	. . . . . . 7 class Cn
12	9, 10, 11	co 6650	. . . . . 6 class ( II Cn x )
13	8, 12	wss 3574	. . . . 5 wff { f , g } C_ ( II Cn x )
14		cphtpy 22767	. . . . . . . 8 class PHtpy
15	10, 14	cfv 5888	. . . . . . 7 class ( PHtpy ` x )
16	5, 7, 15	co 6650	. . . . . 6 class ( f ( PHtpy ` x ) g )
17		c0 3915	. . . . . 6 class (/)
18	16, 17	wne 2794	. . . . 5 wff ( f ( PHtpy ` x ) g ) =/= (/)
19	13, 18	wa 384	. . . 4 wff ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) )
20	19, 4, 6	copab 4712	. . 3 class { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) }
21	2, 3, 20	cmpt 4729	. 2 class ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )
22	1, 21	wceq 1483	1 wff ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )

This definition is referenced by:  phtpcrel  22792  isphtpc  22793