Definition df-phtpy 22770

Description: Define the class of path homotopies between two paths F , G : II --> X; these are homotopies (in the sense of df-htpy 22769) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
df-phtpy	|- PHtpy = ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )

Distinct variable group:   f, g, h, s, x

Detailed syntax breakdown of Definition df-phtpy

Step	Hyp	Ref	Expression
1		cphtpy 22767	. 2 class PHtpy
2		vx	. . 3 setvar x
3		ctop 20698	. . 3 class Top
4		vf	. . . 4 setvar f
5		vg	. . . 4 setvar g
6		cii 22678	. . . . 5 class II
7	2	cv 1482	. . . . 5 class x
8		ccn 21028	. . . . 5 class Cn
9	6, 7, 8	co 6650	. . . 4 class ( II Cn x )
10		cc0 9936	. . . . . . . . 9 class 0
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1482	. . . . . . . . 9 class s
13		vh	. . . . . . . . . 10 setvar h
14	13	cv 1482	. . . . . . . . 9 class h
15	10, 12, 14	co 6650	. . . . . . . 8 class ( 0 h s )
16	4	cv 1482	. . . . . . . . 9 class f
17	10, 16	cfv 5888	. . . . . . . 8 class ( f ` 0 )
18	15, 17	wceq 1483	. . . . . . 7 wff ( 0 h s ) = ( f ` 0 )
19		c1 9937	. . . . . . . . 9 class 1
20	19, 12, 14	co 6650	. . . . . . . 8 class ( 1 h s )
21	19, 16	cfv 5888	. . . . . . . 8 class ( f ` 1 )
22	20, 21	wceq 1483	. . . . . . 7 wff ( 1 h s ) = ( f ` 1 )
23	18, 22	wa 384	. . . . . 6 wff ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) )
24		cicc 12178	. . . . . . 7 class [,]
25	10, 19, 24	co 6650	. . . . . 6 class ( 0 [,] 1 )
26	23, 11, 25	wral 2912	. . . . 5 wff A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) )
27	5	cv 1482	. . . . . 6 class g
28		chtpy 22766	. . . . . . 7 class Htpy
29	6, 7, 28	co 6650	. . . . . 6 class ( II Htpy x )
30	16, 27, 29	co 6650	. . . . 5 class ( f ( II Htpy x ) g )
31	26, 13, 30	crab 2916	. . . 4 class { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) }
32	4, 5, 9, 9, 31	cmpt2 6652	. . 3 class ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } )
33	2, 3, 32	cmpt 4729	. 2 class ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
34	1, 33	wceq 1483	1 wff PHtpy = ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )

This definition is referenced by:  isphtpy  22780