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 = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑟 ∈ ( 𝑗 Cn 𝑘 ) ∣ ∃ 𝑠 ∈ ( 𝑘 Cn 𝑗 ) ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cretr	⊢ Retr
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vk	⊢ 𝑘
4		vr	⊢ 𝑟
5	1	cv	⊢ 𝑗
6		ccn	⊢ Cn
7	3	cv	⊢ 𝑘
8	5 7 6	co	⊢ ( 𝑗 Cn 𝑘 )
9		vs	⊢ 𝑠
10	7 5 6	co	⊢ ( 𝑘 Cn 𝑗 )
11	4	cv	⊢ 𝑟
12	9	cv	⊢ 𝑠
13	11 12	ccom	⊢ ( 𝑟 ∘ 𝑠 )
14		chtpy	⊢ Htpy
15	5 5 14	co	⊢ ( 𝑗 Htpy 𝑗 )
16		cid	⊢ I
17	5	cuni	⊢ ∪ 𝑗
18	16 17	cres	⊢ ( I ↾ ∪ 𝑗 )
19	13 18 15	co	⊢ ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) )
20		c0	⊢ ∅
21	19 20	wne	⊢ ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅
22	21 9 10	wrex	⊢ ∃ 𝑠 ∈ ( 𝑘 Cn 𝑗 ) ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅
23	22 4 8	crab	⊢ { 𝑟 ∈ ( 𝑗 Cn 𝑘 ) ∣ ∃ 𝑠 ∈ ( 𝑘 Cn 𝑗 ) ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅ }
24	1 3 2 2 23	cmpo	⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑟 ∈ ( 𝑗 Cn 𝑘 ) ∣ ∃ 𝑠 ∈ ( 𝑘 Cn 𝑗 ) ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅ } )
25	0 24	wceq	⊢ Retr = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑟 ∈ ( 𝑗 Cn 𝑘 ) ∣ ∃ 𝑠 ∈ ( 𝑘 Cn 𝑗 ) ( ( 𝑟 ∘ 𝑠 ) ( 𝑗 Htpy 𝑗 ) ( I ↾ ∪ 𝑗 ) ) ≠ ∅ } )