Metamath Proof Explorer

Definition df-phtpc

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)

Ref Expression
Assertion df-phtpc ⊢ ≃ ph = x ∈ Top ⟼ f g | f g ⊆ II Cn x ∧ f PHtpy ⁡ x g ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphtpc class ≃ ph
1 vx setvar x
2 ctop class Top
3 vf setvar f
4 vg setvar g
5 3 cv setvar f
6 4 cv setvar g
7 5 6 cpr class f g
8 cii class II
9 ccn class Cn
10 1 cv setvar x
11 8 10 9 co class II Cn x
12 7 11 wss wff f g ⊆ II Cn x
13 cphtpy class PHtpy
14 10 13 cfv class PHtpy ⁡ x
15 5 6 14 co class f PHtpy ⁡ x g
16 c0 class ∅
17 15 16 wne wff f PHtpy ⁡ x g ≠ ∅
18 12 17 wa wff f g ⊆ II Cn x ∧ f PHtpy ⁡ x g ≠ ∅
19 18 3 4 copab class f g | f g ⊆ II Cn x ∧ f PHtpy ⁡ x g ≠ ∅
20 1 2 19 cmpt class x ∈ Top ⟼ f g | f g ⊆ II Cn x ∧ f PHtpy ⁡ x g ≠ ∅
21 0 20 wceq wff ≃ ph = x ∈ Top ⟼ f g | f g ⊆ II Cn x ∧ f PHtpy ⁡ x g ≠ ∅