Definition df-htpy 22769

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.)

Assertion

Ref	Expression
df-htpy	|- Htpy = ( x e. Top , y e. Top |-> ( f e. ( x Cn y ) , g e. ( x Cn y ) |-> { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )

Distinct variable group:   f, g, h, s, x, y

Detailed syntax breakdown of Definition df-htpy

Step	Hyp	Ref	Expression
1		chtpy 22766	. 2 class Htpy
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		ctop 20698	. . 3 class Top
5		vf	. . . 4 setvar f
6		vg	. . . 4 setvar g
7	2	cv 1482	. . . . 5 class x
8	3	cv 1482	. . . . 5 class y
9		ccn 21028	. . . . 5 class Cn
10	7, 8, 9	co 6650	. . . 4 class ( x Cn y )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1482	. . . . . . . . 9 class s
13		cc0 9936	. . . . . . . . 9 class 0
14		vh	. . . . . . . . . 10 setvar h
15	14	cv 1482	. . . . . . . . 9 class h
16	12, 13, 15	co 6650	. . . . . . . 8 class ( s h 0 )
17	5	cv 1482	. . . . . . . . 9 class f
18	12, 17	cfv 5888	. . . . . . . 8 class ( f ` s )
19	16, 18	wceq 1483	. . . . . . 7 wff ( s h 0 ) = ( f ` s )
20		c1 9937	. . . . . . . . 9 class 1
21	12, 20, 15	co 6650	. . . . . . . 8 class ( s h 1 )
22	6	cv 1482	. . . . . . . . 9 class g
23	12, 22	cfv 5888	. . . . . . . 8 class ( g ` s )
24	21, 23	wceq 1483	. . . . . . 7 wff ( s h 1 ) = ( g ` s )
25	19, 24	wa 384	. . . . . 6 wff ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) )
26	7	cuni 4436	. . . . . 6 class U. x
27	25, 11, 26	wral 2912	. . . . 5 wff A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) )
28		cii 22678	. . . . . . 7 class II
29		ctx 21363	. . . . . . 7 class tX
30	7, 28, 29	co 6650	. . . . . 6 class ( x tX II )
31	30, 8, 9	co 6650	. . . . 5 class ( ( x tX II ) Cn y )
32	27, 14, 31	crab 2916	. . . 4 class { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) }
33	5, 6, 10, 10, 32	cmpt2 6652	. . 3 class ( f e. ( x Cn y ) , g e. ( x Cn y ) |-> { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } )
34	2, 3, 4, 4, 33	cmpt2 6652	. 2 class ( x e. Top , y e. Top |-> ( f e. ( x Cn y ) , g e. ( x Cn y ) |-> { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )
35	1, 34	wceq 1483	1 wff Htpy = ( x e. Top , y e. Top |-> ( f e. ( x Cn y ) , g e. ( x Cn y ) |-> { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )

This definition is referenced by:  ishtpy  22771