Definition df-phtpy

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

	Ref	Expression
Assertion	df-phtpy	⊢ PHtpy = ( 𝑥 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑥 ) , 𝑔 ∈ ( II Cn 𝑥 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphtpy	⊢ PHtpy
1		vx	⊢ 𝑥
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		cii	⊢ II
5		ccn	⊢ Cn
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( II Cn 𝑥 )
8		vg	⊢ 𝑔
9		vh	⊢ ℎ
10	3	cv	⊢ 𝑓
11		chtpy	⊢ Htpy
12	4 6 11	co	⊢ ( II Htpy 𝑥 )
13	8	cv	⊢ 𝑔
14	10 13 12	co	⊢ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 )
15		vs	⊢ 𝑠
16		cc0	⊢ 0
17		cicc	⊢ [,]
18		c1	⊢ 1
19	16 18 17	co	⊢ ( 0 [,] 1 )
20	9	cv	⊢ ℎ
21	15	cv	⊢ 𝑠
22	16 21 20	co	⊢ ( 0 ℎ 𝑠 )
23	16 10	cfv	⊢ ( 𝑓 ‘ 0 )
24	22 23	wceq	⊢ ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 )
25	18 21 20	co	⊢ ( 1 ℎ 𝑠 )
26	18 10	cfv	⊢ ( 𝑓 ‘ 1 )
27	25 26	wceq	⊢ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 )
28	24 27	wa	⊢ ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) )
29	28 15 19	wral	⊢ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) )
30	29 9 14	crab	⊢ { ℎ ∈ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) }
31	3 8 7 7 30	cmpo	⊢ ( 𝑓 ∈ ( II Cn 𝑥 ) , 𝑔 ∈ ( II Cn 𝑥 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } )
32	1 2 31	cmpt	⊢ ( 𝑥 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑥 ) , 𝑔 ∈ ( II Cn 𝑥 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )
33	0 32	wceq	⊢ PHtpy = ( 𝑥 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑥 ) , 𝑔 ∈ ( II Cn 𝑥 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑥 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )