Metamath Proof Explorer

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 = x ∈ Top ⟼ f ∈ II Cn x , g ∈ II Cn x ⟼ h ∈ f II Htpy x g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphtpy class PHtpy
1 vx setvar x
2 ctop class Top
3 vf setvar f
4 cii class II
5 ccn class Cn
6 1 cv setvar x
7 4 6 5 co class II Cn x
8 vg setvar g
9 vh setvar h
10 3 cv setvar f
11 chtpy class Htpy
12 4 6 11 co class II Htpy x
13 8 cv setvar g
14 10 13 12 co class f II Htpy x g
15 vs setvar s
16 cc0 class 0
17 cicc class .
18 c1 class 1
19 16 18 17 co class 0 1
20 9 cv setvar h
21 15 cv setvar s
22 16 21 20 co class 0 h s
23 16 10 cfv class f ⁡ 0
24 22 23 wceq wff 0 h s = f ⁡ 0
25 18 21 20 co class 1 h s
26 18 10 cfv class f ⁡ 1
27 25 26 wceq wff 1 h s = f ⁡ 1
28 24 27 wa wff 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
29 28 15 19 wral wff ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
30 29 9 14 crab class h ∈ f II Htpy x g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
31 3 8 7 7 30 cmpo class f ∈ II Cn x , g ∈ II Cn x ⟼ h ∈ f II Htpy x g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
32 1 2 31 cmpt class x ∈ Top ⟼ f ∈ II Cn x , g ∈ II Cn x ⟼ h ∈ f II Htpy x g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
33 0 32 wceq wff PHtpy = x ∈ Top ⟼ f ∈ II Cn x , g ∈ II Cn x ⟼ h ∈ f II Htpy x g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1