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 \in Top ⟼ (f \in (II Cn x), g \in (II Cn x) ⟼ \{h \in (f (II Htpy x) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 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) \land 1 h s = f (1))$
29	28 15 19	wral	$wff \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))$
30	29 9 14	crab	$class \{h \in (f (II Htpy x) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}$
31	3 8 7 7 30	cmpo	$class (f \in (II Cn x), g \in (II Cn x) ⟼ \{h \in (f (II Htpy x) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\})$
32	1 2 31	cmpt	$class (x \in Top ⟼ (f \in (II Cn x), g \in (II Cn x) ⟼ \{h \in (f (II Htpy x) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}))$
33	0 32	wceq	$wff PHtpy = (x \in Top ⟼ (f \in (II Cn x), g \in (II Cn x) ⟼ \{h \in (f (II Htpy x) g) \| \forall s \in [0, 1] (0 h s = f (0) \land 1 h s = f (1))\}))$

Metamath Proof Explorer

Definition df-phtpy

Detailed syntax breakdown