Definition df-retr 31799

Description: Define the set of retractions on two topological spaces. We say that 𝑅 is a retraction from 𝐽 to 𝐾. or 𝑅 ∈ (𝐽 Retr 𝐾) iff there is an 𝑆 such that 𝑅:𝐽⟶𝐾, 𝑆:𝐾⟶𝐽 are continuous functions called the retraction and section respectively, and their composite 𝑅 ∘ 𝑆 is homotopic to the identity map. If a retraction exists, we say 𝐽 is a retract of 𝐾. (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.)

Assertion

Ref	Expression
df-retr	⊢ Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅})

Distinct variable group:   𝑗,𝑘,𝑟,𝑠

Detailed syntax breakdown of Definition df-retr

Step	Hyp	Ref	Expression
1		cretr 31798	. 2 class Retr
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 21105	. . 3 class Top
5		vr	. . . . . . . . 9 setvar 𝑟
6	5	cv 1600	. . . . . . . 8 class 𝑟
7		vs	. . . . . . . . 9 setvar 𝑠
8	7	cv 1600	. . . . . . . 8 class 𝑠
9	6, 8	ccom 5359	. . . . . . 7 class (𝑟 ∘ 𝑠)
10		cid 5260	. . . . . . . 8 class I
11	2	cv 1600	. . . . . . . . 9 class 𝑗
12	11	cuni 4671	. . . . . . . 8 class ∪ 𝑗
13	10, 12	cres 5357	. . . . . . 7 class ( I ↾ ∪ 𝑗)
14		chtpy 23174	. . . . . . . 8 class Htpy
15	11, 11, 14	co 6922	. . . . . . 7 class (𝑗 Htpy 𝑗)
16	9, 13, 15	co 6922	. . . . . 6 class ((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗))
17		c0 4140	. . . . . 6 class ∅
18	16, 17	wne 2968	. . . . 5 wff ((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅
19	3	cv 1600	. . . . . 6 class 𝑘
20		ccn 21436	. . . . . 6 class Cn
21	19, 11, 20	co 6922	. . . . 5 class (𝑘 Cn 𝑗)
22	18, 7, 21	wrex 3090	. . . 4 wff ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅
23	11, 19, 20	co 6922	. . . 4 class (𝑗 Cn 𝑘)
24	22, 5, 23	crab 3093	. . 3 class {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅}
25	2, 3, 4, 4, 24	cmpt2 6924	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅})
26	1, 25	wceq 1601	1 wff Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅})

This definition is referenced by: (None)