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	$$⊢\mathrm{Retr}=\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{r\in \left(j\mathrm{Cn}k\right)|\exists s\in \left(k\mathrm{Cn}j\right)\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing \right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cretr	$$class\mathrm{Retr}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vk	$$setvark$$
4		vr	$$setvarr$$
5	1	cv	$$setvarj$$
6		ccn	$$class\mathrm{Cn}$$
7	3	cv	$$setvark$$
8	5 7 6	co	$$class\left(j\mathrm{Cn}k\right)$$
9		vs	$$setvars$$
10	7 5 6	co	$$class\left(k\mathrm{Cn}j\right)$$
11	4	cv	$$setvarr$$
12	9	cv	$$setvars$$
13	11 12	ccom	$$class\left(r\circ s\right)$$
14		chtpy	$$class\mathrm{Htpy}$$
15	5 5 14	co	$$class\left(j\mathrm{Htpy}j\right)$$
16		cid	$$class\mathrm{I}$$
17	5	cuni	$$class\bigcup j$$
18	16 17	cres	$$class\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)$$
19	13 18 15	co	$$class\left(\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\right)$$
20		c0	$$class\varnothing$$
21	19 20	wne	$$wff\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing$$
22	21 9 10	wrex	$$wff\exists s\in \left(k\mathrm{Cn}j\right)\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing$$
23	22 4 8	crab	$$class\left\{r\in \left(j\mathrm{Cn}k\right)|\exists s\in \left(k\mathrm{Cn}j\right)\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing \right\}$$
24	1 3 2 2 23	cmpo	$$class\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{r\in \left(j\mathrm{Cn}k\right)|\exists s\in \left(k\mathrm{Cn}j\right)\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing \right\}\right)$$
25	0 24	wceq	$$wff\mathrm{Retr}=\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{r\in \left(j\mathrm{Cn}k\right)|\exists s\in \left(k\mathrm{Cn}j\right)\left(r\circ s\right)\left(j\mathrm{Htpy}j\right)\left({\mathrm{I}\upharpoonright }_{\bigcup j}\right)\ne \varnothing \right\}\right)$$