Definition df-phtpy 22578

Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 22577) 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 22575	. 2 class PHtpy
2		vx	. . 3 setvar 𝑥
3		ctop 20517	. . 3 class Top
4		vf	. . . 4 setvar 𝑓
5		vg	. . . 4 setvar 𝑔
6		cii 22486	. . . . 5 class II
7	2	cv 1474	. . . . 5 class 𝑥
8		ccn 20838	. . . . 5 class Cn
9	6, 7, 8	co 6549	. . . 4 class (II Cn 𝑥)
10		cc0 9815	. . . . . . . . 9 class 0
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1474	. . . . . . . . 9 class 𝑠
13		vh	. . . . . . . . . 10 setvar ℎ
14	13	cv 1474	. . . . . . . . 9 class ℎ
15	10, 12, 14	co 6549	. . . . . . . 8 class (0ℎ𝑠)
16	4	cv 1474	. . . . . . . . 9 class 𝑓
17	10, 16	cfv 5804	. . . . . . . 8 class (𝑓‘0)
18	15, 17	wceq 1475	. . . . . . 7 wff (0ℎ𝑠) = (𝑓‘0)
19		c1 9816	. . . . . . . . 9 class 1
20	19, 12, 14	co 6549	. . . . . . . 8 class (1ℎ𝑠)
21	19, 16	cfv 5804	. . . . . . . 8 class (𝑓‘1)
22	20, 21	wceq 1475	. . . . . . 7 wff (1ℎ𝑠) = (𝑓‘1)
23	18, 22	wa 383	. . . . . 6 wff ((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
24		cicc 12049	. . . . . . 7 class [,]
25	10, 19, 24	co 6549	. . . . . 6 class (0[,]1)
26	23, 11, 25	wral 2896	. . . . 5 wff ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
27	5	cv 1474	. . . . . 6 class 𝑔
28		chtpy 22574	. . . . . . 7 class Htpy
29	6, 7, 28	co 6549	. . . . . 6 class (II Htpy 𝑥)
30	16, 27, 29	co 6549	. . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
31	26, 13, 30	crab 2900	. . . 4 class {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}
32	4, 5, 9, 9, 31	cmpt2 6551	. . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})
33	2, 3, 32	cmpt 4643	. 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))
34	1, 33	wceq 1475	1 wff PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))

This definition is referenced by:  isphtpy  22588