Definition df-retr

Description: Define the set of retractions on two topological spaces. We say that R is a retraction from J to K . or R e. ( J Retr K ) iff there is an S such that R : J --> K , S : K --> J are continuous functions called the retraction and section respectively, and their composite R o. S is homotopic to the identity map. If a retraction exists, we say J is a retract of K . (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	df-retr	|- Retr = ( j e. Top , k e. Top |-> { r e. ( j Cn k ) | E. s e. ( k Cn j ) ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cretr	|- Retr
1		vj	|- j
2		ctop	|- Top
3		vk	|- k
4		vr	|- r
5	1	cv	|- j
6		ccn	|- Cn
7	3	cv	|- k
8	5 7 6	co	|- ( j Cn k )
9		vs	|- s
10	7 5 6	co	|- ( k Cn j )
11	4	cv	|- r
12	9	cv	|- s
13	11 12	ccom	|- ( r o. s )
14		chtpy	|- Htpy
15	5 5 14	co	|- ( j Htpy j )
16		cid	|- _I
17	5	cuni	|- U. j
18	16 17	cres	|- ( _I |` U. j )
19	13 18 15	co	|- ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) )
20		c0	|- (/)
21	19 20	wne	|- ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/)
22	21 9 10	wrex	|- E. s e. ( k Cn j ) ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/)
23	22 4 8	crab	|- { r e. ( j Cn k ) | E. s e. ( k Cn j ) ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/) }
24	1 3 2 2 23	cmpo	|- ( j e. Top , k e. Top |-> { r e. ( j Cn k ) | E. s e. ( k Cn j ) ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/) } )
25	0 24	wceq	|- Retr = ( j e. Top , k e. Top |-> { r e. ( j Cn k ) | E. s e. ( k Cn j ) ( ( r o. s ) ( j Htpy j ) ( _I |` U. j ) ) =/= (/) } )