Definition df-phtpy 24040

Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 24039) 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 24037	. 2 class PHtpy
2		vx	. . 3 setvar 𝑥
3		ctop 21950	. . 3 class Top
4		vf	. . . 4 setvar 𝑓
5		vg	. . . 4 setvar 𝑔
6		cii 23944	. . . . 5 class II
7	2	cv 1538	. . . . 5 class 𝑥
8		ccn 22283	. . . . 5 class Cn
9	6, 7, 8	co 7255	. . . 4 class (II Cn 𝑥)
10		cc0 10802	. . . . . . . . 9 class 0
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1538	. . . . . . . . 9 class 𝑠
13		vh	. . . . . . . . . 10 setvar ℎ
14	13	cv 1538	. . . . . . . . 9 class ℎ
15	10, 12, 14	co 7255	. . . . . . . 8 class (0ℎ𝑠)
16	4	cv 1538	. . . . . . . . 9 class 𝑓
17	10, 16	cfv 6418	. . . . . . . 8 class (𝑓‘0)
18	15, 17	wceq 1539	. . . . . . 7 wff (0ℎ𝑠) = (𝑓‘0)
19		c1 10803	. . . . . . . . 9 class 1
20	19, 12, 14	co 7255	. . . . . . . 8 class (1ℎ𝑠)
21	19, 16	cfv 6418	. . . . . . . 8 class (𝑓‘1)
22	20, 21	wceq 1539	. . . . . . 7 wff (1ℎ𝑠) = (𝑓‘1)
23	18, 22	wa 395	. . . . . 6 wff ((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
24		cicc 13011	. . . . . . 7 class [,]
25	10, 19, 24	co 7255	. . . . . 6 class (0[,]1)
26	23, 11, 25	wral 3063	. . . . 5 wff ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))
27	5	cv 1538	. . . . . 6 class 𝑔
28		chtpy 24036	. . . . . . 7 class Htpy
29	6, 7, 28	co 7255	. . . . . 6 class (II Htpy 𝑥)
30	16, 27, 29	co 7255	. . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
31	26, 13, 30	crab 3067	. . . 4 class {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}
32	4, 5, 9, 9, 31	cmpo 7257	. . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})
33	2, 3, 32	cmpt 5153	. 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))
34	1, 33	wceq 1539	1 wff PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}))

This definition is referenced by:  isphtpy  24050