df-htpy

Description: Define the function which takes topological spaces X , Y and two continuous functions F , G : X --> Y and returns the class of homotopies from F to G . (Contributed by Mario Carneiro, 22-Feb-2015)

		Ref	Expression
	Assertion	df-htpy	$⊢ Htpy = (x \in Top, y \in Top ⟼ (f \in (x Cn y), g \in (x Cn y) ⟼ \{h \in ((x \times_{t} II) Cn y) \| \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chtpy	$class Htpy$
1		vx	$setvar x$
2		ctop	$class Top$
3		vy	$setvar y$
4		vf	$setvar f$
5	1	cv	$setvar x$
6		ccn	$class Cn$
7	3	cv	$setvar y$
8	5 7 6	co	$class (x Cn y)$
9		vg	$setvar g$
10		vh	$setvar h$
11		ctx	$class \times_{t}$
12		cii	$class II$
13	5 12 11	co	$class (x \times_{t} II)$
14	13 7 6	co	$class ((x \times_{t} II) Cn y)$
15		vs	$setvar s$
16	5	cuni	$class ⋃ x$
17	15	cv	$setvar s$
18	10	cv	$setvar h$
19		cc0	$class 0$
20	17 19 18	co	$class (s h 0)$
21	4	cv	$setvar f$
22	17 21	cfv	$class f (s)$
23	20 22	wceq	$wff s h 0 = f (s)$
24		c1	$class 1$
25	17 24 18	co	$class (s h 1)$
26	9	cv	$setvar g$
27	17 26	cfv	$class g (s)$
28	25 27	wceq	$wff s h 1 = g (s)$
29	23 28	wa	$wff (s h 0 = f (s) \land s h 1 = g (s))$
30	29 15 16	wral	$wff \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))$
31	30 10 14	crab	$class \{h \in ((x \times_{t} II) Cn y) \| \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))\}$
32	4 9 8 8 31	cmpo	$class (f \in (x Cn y), g \in (x Cn y) ⟼ \{h \in ((x \times_{t} II) Cn y) \| \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))\})$
33	1 3 2 2 32	cmpo	$class (x \in Top, y \in Top ⟼ (f \in (x Cn y), g \in (x Cn y) ⟼ \{h \in ((x \times_{t} II) Cn y) \| \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))\}))$
34	0 33	wceq	$wff Htpy = (x \in Top, y \in Top ⟼ (f \in (x Cn y), g \in (x Cn y) ⟼ \{h \in ((x \times_{t} II) Cn y) \| \forall s \in ⋃ x (s h 0 = f (s) \land s h 1 = g (s))\}))$

Metamath Proof Explorer

Definition df-htpy

Detailed syntax breakdown