Definition df-htpy 22577

Description: Define the function which takes topological spaces 𝑋, 𝑌 and two continuous functions 𝐹, 𝐺:𝑋⟶𝑌 and returns the class of homotopies from 𝐹 to 𝐺. (Contributed by Mario Carneiro, 22-Feb-2015.)

Assertion

Ref	Expression
df-htpy	⊢ Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}))

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

Detailed syntax breakdown of Definition df-htpy

Step	Hyp	Ref	Expression
1		chtpy 22574	. 2 class Htpy
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		ctop 20517	. . 3 class Top
5		vf	. . . 4 setvar 𝑓
6		vg	. . . 4 setvar 𝑔
7	2	cv 1474	. . . . 5 class 𝑥
8	3	cv 1474	. . . . 5 class 𝑦
9		ccn 20838	. . . . 5 class Cn
10	7, 8, 9	co 6549	. . . 4 class (𝑥 Cn 𝑦)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1474	. . . . . . . . 9 class 𝑠
13		cc0 9815	. . . . . . . . 9 class 0
14		vh	. . . . . . . . . 10 setvar ℎ
15	14	cv 1474	. . . . . . . . 9 class ℎ
16	12, 13, 15	co 6549	. . . . . . . 8 class (𝑠ℎ0)
17	5	cv 1474	. . . . . . . . 9 class 𝑓
18	12, 17	cfv 5804	. . . . . . . 8 class (𝑓‘𝑠)
19	16, 18	wceq 1475	. . . . . . 7 wff (𝑠ℎ0) = (𝑓‘𝑠)
20		c1 9816	. . . . . . . . 9 class 1
21	12, 20, 15	co 6549	. . . . . . . 8 class (𝑠ℎ1)
22	6	cv 1474	. . . . . . . . 9 class 𝑔
23	12, 22	cfv 5804	. . . . . . . 8 class (𝑔‘𝑠)
24	21, 23	wceq 1475	. . . . . . 7 wff (𝑠ℎ1) = (𝑔‘𝑠)
25	19, 24	wa 383	. . . . . 6 wff ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))
26	7	cuni 4372	. . . . . 6 class ∪ 𝑥
27	25, 11, 26	wral 2896	. . . . 5 wff ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))
28		cii 22486	. . . . . . 7 class II
29		ctx 21173	. . . . . . 7 class ×t
30	7, 28, 29	co 6549	. . . . . 6 class (𝑥 ×t II)
31	30, 8, 9	co 6549	. . . . 5 class ((𝑥 ×t II) Cn 𝑦)
32	27, 14, 31	crab 2900	. . . 4 class {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}
33	5, 6, 10, 10, 32	cmpt2 6551	. . 3 class (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))})
34	2, 3, 4, 4, 33	cmpt2 6551	. 2 class (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}))
35	1, 34	wceq 1475	1 wff Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}))

This definition is referenced by:  ishtpy  22579