Definition df-phtpy 24468

Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 24467) 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 = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))

Distinct variable group:   𝑓,𝑔,ℎ,𝑠,𝑥

Detailed syntax breakdown of Definition df-phtpy

Step	Hyp	Ref	Expression
1		cphtpy 24465	. 2 class PHtpy
2		vx	. . 3 setvar 𝑥
3		ctop 22376	. . 3 class Top
4		vf	. . . 4 setvar 𝑓
5		vg	. . . 4 setvar 𝑔
6		cii 24372	. . . . 5 class II
7	2	cv 1541	. . . . 5 class 𝑥
8		ccn 22709	. . . . 5 class Cn
9	6, 7, 8	co 7403	. . . 4 class (II Cn 𝑥)
10		cc0 11105	. . . . . . . . 9 class 0
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1541	. . . . . . . . 9 class 𝑠
13		vh	. . . . . . . . . 10 setvar ℎ
14	13	cv 1541	. . . . . . . . 9 class ℎ
15	10, 12, 14	co 7403	. . . . . . . 8 class (0ℎ𝑠)
16	4	cv 1541	. . . . . . . . 9 class 𝑓
17	10, 16	cfv 6539	. . . . . . . 8 class (𝑓‘0)
18	15, 17	wceq 1542	. . . . . . 7 wff (0ℎ𝑠) = (𝑓‘0)
19		c1 11106	. . . . . . . . 9 class 1
20	19, 12, 14	co 7403	. . . . . . . 8 class (1ℎ𝑠)
21	19, 16	cfv 6539	. . . . . . . 8 class (𝑓‘1)
22	20, 21	wceq 1542	. . . . . . 7 wff (1ℎ𝑠) = (𝑓‘1)
23	18, 22	wa 397	. . . . . 6 wff ((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
24		cicc 13322	. . . . . . 7 class [,]
25	10, 19, 24	co 7403	. . . . . 6 class (0[,]1)
26	23, 11, 25	wral 3062	. . . . 5 wff ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
27	5	cv 1541	. . . . . 6 class 𝑔
28		chtpy 24464	. . . . . . 7 class Htpy
29	6, 7, 28	co 7403	. . . . . 6 class (II Htpy 𝑥)
30	16, 27, 29	co 7403	. . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
31	26, 13, 30	crab 3433	. . . 4 class {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}
32	4, 5, 9, 9, 31	cmpo 7405	. . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})
33	2, 3, 32	cmpt 5229	. 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))
34	1, 33	wceq 1542	1 wff PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))

This definition is referenced by:  isphtpy  24478