Definition df-phtpc 24061

Description: Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)

Assertion

Ref	Expression
df-phtpc	⊢ ≃ph = (𝑥 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)})

Distinct variable group:   𝑥,𝑓,𝑔

Detailed syntax breakdown of Definition df-phtpc

Step	Hyp	Ref	Expression
1		cphtpc 24038	. 2 class ≃ph
2		vx	. . 3 setvar 𝑥
3		ctop 21950	. . 3 class Top
4		vf	. . . . . . . 8 setvar 𝑓
5	4	cv 1538	. . . . . . 7 class 𝑓
6		vg	. . . . . . . 8 setvar 𝑔
7	6	cv 1538	. . . . . . 7 class 𝑔
8	5, 7	cpr 4560	. . . . . 6 class {𝑓, 𝑔}
9		cii 23944	. . . . . . 7 class II
10	2	cv 1538	. . . . . . 7 class 𝑥
11		ccn 22283	. . . . . . 7 class Cn
12	9, 10, 11	co 7255	. . . . . 6 class (II Cn 𝑥)
13	8, 12	wss 3883	. . . . 5 wff {𝑓, 𝑔} ⊆ (II Cn 𝑥)
14		cphtpy 24037	. . . . . . . 8 class PHtpy
15	10, 14	cfv 6418	. . . . . . 7 class (PHtpy‘𝑥)
16	5, 7, 15	co 7255	. . . . . 6 class (𝑓(PHtpy‘𝑥)𝑔)
17		c0 4253	. . . . . 6 class ∅
18	16, 17	wne 2942	. . . . 5 wff (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅
19	13, 18	wa 395	. . . 4 wff ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)
20	19, 4, 6	copab 5132	. . 3 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)}
21	2, 3, 20	cmpt 5153	. 2 class (𝑥 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)})
22	1, 21	wceq 1539	1 wff ≃ph = (𝑥 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)})

This definition is referenced by:  phtpcrel  24062  isphtpc  24063